proposition: Lemma asimpl_up_scons X (t:X) s : S >> (t .: s) ≡ s.
proof: Proof. now intros [|n]. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid