proposition: Lemma compComp'_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) : funcomp (subst_exp tauexp) (subst_exp sigmaexp) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) .
proof: Proof. exact (FunctionalExtensionality.functional_extensionality _ _ (fun n => compComp_exp sigmaexp tauexp n)). Qed.
imports: Undecidability.HOU(std.std)