fact: Fixpoint compSubstRen__exp (sigmaexp : fin -> exp ) (zetaexp : fin -> fin ) (thetaexp : fin -> exp ) (Eqexp : forall x, (funcomp (ren_exp zetaexp) sigmaexp) x = thetaexp x) (s : exp ) : ren_exp zetaexp (subst_exp sigmaexp s) = subst_exp thetaexp s := match s with | var_exp s => Eqexp s | const s0 => congr_const (eq_refl s0) | lam s0 => congr_lam (compSubstRen__exp (up_exp_exp sigmaexp) (upRen_exp_exp zetaexp) (up_exp_exp thetaexp) (up_subst_ren_exp_exp (_) (_) (_) Eqexp) s0) | app s0 s1 => congr_app (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s0) (compSubstRen__exp sigmaexp zetaexp thetaexp Eqexp s1) end.
imports: Undecidability.HOU(std.std)