fact: Fixpoint ext_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (taupoly_type : ( nat ) -> poly_type ) (tauterm : ( nat ) -> term ) (Eqpoly_type : forall x, sigmapoly_type x = taupoly_type x) (Eqterm : forall x, sigmaterm x = tauterm x) (s : term ) : subst_term sigmapoly_type sigmaterm s = subst_term taupoly_type tauterm s := match s return subst_term sigmapoly_type sigmaterm s = subst_term taupoly_type tauterm s with | var s => Eqterm s | app s0 s1 => congr_app (ext_term sigmapoly_type sigmaterm taupoly_type tauterm Eqpoly_type Eqterm s0) (ext_term sigmapoly_type sigmaterm taupoly_type tauterm Eqpoly_type Eqterm s1) | abs s0 s1 => congr_abs (ext_poly_type sigmapoly_type taupoly_type Eqpoly_type s0) (ext_term (up_term_poly_type sigmapoly_type) (up_term_term sigmaterm) (up_term_poly_type taupoly_type) (up_term_term tauterm) (upExt_term_poly_type (_) (_) Eqpoly_type) (upExt_term_term (_) (_) Eqterm) s1) | ty_app s0 s1 => congr_ty_app (ext_term sigmapoly_type sigmaterm taupoly_type tauterm Eqpoly_type Eqterm s0) (ext_poly_type sigmapoly_type taupoly_type Eqpoly_type s1) | ty_abs s0 => congr_ty_abs (ext_term (up_poly_type_poly_type sigmapoly_type) (up_poly_type_term sigmaterm) (up_poly_type_poly_type taupoly_type) (up_poly_type_term tauterm) (upExt_poly_type_poly_type (_) (_) Eqpoly_type) (upExt_poly_type_term (_) (_) Eqterm) s0) end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms