fact: Fixpoint compRenRen_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) (zetapoly_type : ( nat ) -> nat ) (zetaterm : ( nat ) -> nat ) (rhopoly_type : ( nat ) -> nat ) (rhoterm : ( nat ) -> nat ) (Eqpoly_type : forall x, (funcomp zetapoly_type xipoly_type) x = rhopoly_type x) (Eqterm : forall x, (funcomp zetaterm xiterm) x = rhoterm x) (s : term ) : ren_term zetapoly_type zetaterm (ren_term xipoly_type xiterm s) = ren_term rhopoly_type rhoterm s := match s return ren_term zetapoly_type zetaterm (ren_term xipoly_type xiterm s) = ren_term rhopoly_type rhoterm s with | var s => ap (var ) (Eqterm s) | app s0 s1 => congr_app (compRenRen_term xipoly_type xiterm zetapoly_type zetaterm rhopoly_type rhoterm Eqpoly_type Eqterm s0) (compRenRen_term xipoly_type xiterm zetapoly_type zetaterm rhopoly_type rhoterm Eqpoly_type Eqterm s1) | abs s0 s1 => congr_abs (compRenRen_poly_type xipoly_type zetapoly_type rhopoly_type Eqpoly_type s0) (compRenRen_term (upRen_term_poly_type xipoly_type) (upRen_term_term xiterm) (upRen_term_poly_type zetapoly_type) (upRen_term_term zetaterm) (upRen_term_poly_type rhopoly_type) (upRen_term_term rhoterm) Eqpoly_type (up_ren_ren_term_term (_) (_) (_) Eqterm) s1) | ty_app s0 s1 => congr_ty_app (compRenRen_term xipoly_type xiterm zetapoly_type zetaterm rhopoly_type rhoterm Eqpoly_type Eqterm s0) (compRenRen_poly_type xipoly_type zetapoly_type rhopoly_type Eqpoly_type s1) | ty_abs s0 => congr_ty_abs (compRenRen_term (upRen_poly_type_poly_type xipoly_type) (upRen_poly_type_term xiterm) (upRen_poly_type_poly_type zetapoly_type) (upRen_poly_type_term zetaterm) (upRen_poly_type_poly_type rhopoly_type) (upRen_poly_type_term rhoterm) (up_ren_ren_poly_type_poly_type (_) (_) (_) Eqpoly_type) Eqterm s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms