some more congruence properties for refexive transitive closure of type reduction and missing cases for ren and sub
trans/concat for reductions
congruence of lambda and pi for reflexive transitive closure of type reduction
new soundness proof for normalisation: referring to reduction instead of beta-eta-equality
substitution by less reduced term in SR. This is baked into the definition in the new equations paper.
potential definition of SR, inlining beta
completeness of the normal typed version with respect to the syntactic typed version done