proposition: Lemma singletonSubst_algebraic : forall G T, isSingletonSubst T G -> algebraic T -> algebraicSubstitution G.
proof: Proof. intros; intros p M D. destruct H. destruct p. replace M with T; trivial. inversion H; inversion D; try_solve. set (hint := H1 p). inversion D; inversion hint; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)