Cardano Updates

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.

• an alternative proof of the first monad law for normal subst which might work with beta-eta if necessary

potential definition of SR, inlining beta

completeness of the normal typed version with respect to the syntactic typed version done