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