proposition: Lemma algebraic_morph_aux : forall x1 x2 : Term, x1 ~ x2 -> (algebraic x1 -> algebraic x2).
proof: Proof. intro t. apply well_founded_ind with (R := subterm) (P := fun t => forall s, t ~ s -> algebraic t -> algebraic s). apply subterm_wf. clear t; intros t IH s ts t_alg. inversion t_alg. apply AlgVar. rewrite <- ts; trivial. set (s_abs := proj1 (isAbs_morph ts) Mabs). apply AlgAbs with s_abs; trivial. apply IH with (absBody Mabs); trivial. apply absBody_subterm. apply abs_conv_absBody; trivial. apply AlgApp. rewrite <- ts; trivial. rewrite <- ts; trivial. intros. destruct (terms_conv_sym ts) as [Q st]. destruct (appUnit_conv_appUnit M' st) as [N' [N't M'N']]; trivial. apply IH with N'. apply appUnit_subterm; trivial. apply terms_conv_sym; exists Q; trivial. apply H1; trivial. apply AlgFunApp. rewrite <- ts; trivial. rewrite <- (terms_conv_eq_type ts); trivial. intros. destruct (terms_conv_sym ts) as [Q st]. destruct (appArg_conv_appArg M' st) as [N' [N't M'N']]; trivial. apply IH with N'. apply arg_subterm; trivial. apply terms_conv_sym; exists Q; trivial. apply H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)