proposition: Lemma algebraicSubstitution_cons_some : forall G T, algebraicSubstitution G -> algebraic T -> algebraicSubstitution (Some T :: G).
proof: Proof. intros; intros p M D. destruct p. inversion D. rewrite <- H2; trivial. apply (H p); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)