proposition: Lemma algebraicSubstitution_cons_none : forall G, algebraicSubstitution G -> algebraicSubstitution (None :: G).
proof: Proof. intros; intros p M D. destruct p. inversion D. apply (H p); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)