fact: Fixpoint compSubstSubst_pure_term (sigmapure_term : ( nat ) -> pure_term ) (taupure_term : ( nat ) -> pure_term ) (thetapure_term : ( nat ) -> pure_term ) (Eqpure_term : forall x, (funcomp (subst_pure_term taupure_term) sigmapure_term) x = thetapure_term x) (s : pure_term ) : subst_pure_term taupure_term (subst_pure_term sigmapure_term s) = subst_pure_term thetapure_term s := match s return subst_pure_term taupure_term (subst_pure_term sigmapure_term s) = subst_pure_term thetapure_term s with | pure_var s => Eqpure_term s | pure_app s0 s1 => congr_pure_app (compSubstSubst_pure_term sigmapure_term taupure_term thetapure_term Eqpure_term s0) (compSubstSubst_pure_term sigmapure_term taupure_term thetapure_term Eqpure_term s1) | pure_abs s0 => congr_pure_abs (compSubstSubst_pure_term (up_pure_term_pure_term sigmapure_term) (up_pure_term_pure_term taupure_term) (up_pure_term_pure_term thetapure_term) (up_subst_subst_pure_term_pure_term (_) (_) (_) Eqpure_term) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms