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