fact: Fixpoint compRenRen_exp (xiexp : fin -> fin ) (zetaexp : fin -> fin ) (rhoexp : fin -> fin ) (Eqexp : forall x, (funcomp zetaexp xiexp) x = rhoexp x) (s : exp ) : ren_exp zetaexp (ren_exp xiexp s) = ren_exp rhoexp s := match s with | var_exp s => ap (var_exp ) (Eqexp s) | const s0 => congr_const (eq_refl s0) | lam s0 => congr_lam (compRenRen_exp (upRen_exp_exp xiexp) (upRen_exp_exp zetaexp) (upRen_exp_exp rhoexp) (up_ren_ren (_) (_) (_) Eqexp) s0) | app s0 s1 => congr_app (compRenRen_exp xiexp zetaexp rhoexp Eqexp s0) (compRenRen_exp xiexp zetaexp rhoexp Eqexp s1) end.
imports: Undecidability.HOU(std.std)