Challenge 1a: Properties of sn
Challenge 1b: Soundness of inductive definition of strongly normalizing terms
Challenge 2a: Properties of Strong Normalization
Challenge 2b: Strong Normalization Proof using Logical Predicate