proposition: Lemma compComp_exp (sigmaexp : fin -> exp ) (tauexp : fin -> exp ) (s : exp ) : subst_exp tauexp (subst_exp sigmaexp s) = subst_exp (funcomp (subst_exp tauexp) sigmaexp) s .
proof: Proof. exact (compSubstSubst_exp sigmaexp tauexp (_) (fun n => eq_refl) s). Qed.
imports: Undecidability.HOU(std.std)