fact: Fixpoint compRenRen_pure_term (xipure_term : ( nat ) -> nat ) (zetapure_term : ( nat ) -> nat ) (rhopure_term : ( nat ) -> nat ) (Eqpure_term : forall x, (funcomp zetapure_term xipure_term) x = rhopure_term x) (s : pure_term ) : ren_pure_term zetapure_term (ren_pure_term xipure_term s) = ren_pure_term rhopure_term s := match s return ren_pure_term zetapure_term (ren_pure_term xipure_term s) = ren_pure_term rhopure_term s with | pure_var s => ap (pure_var ) (Eqpure_term s) | pure_app s0 s1 => congr_pure_app (compRenRen_pure_term xipure_term zetapure_term rhopure_term Eqpure_term s0) (compRenRen_pure_term xipure_term zetapure_term rhopure_term Eqpure_term s1) | pure_abs s0 => congr_pure_abs (compRenRen_pure_term (upRen_pure_term_pure_term xipure_term) (upRen_pure_term_pure_term zetapure_term) (upRen_pure_term_pure_term rhopure_term) (up_ren_ren_pure_term_pure_term (_) (_) (_) Eqpure_term) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms