proposition: Lemma deletion : forall {A B} (t : A), B -> (t = t -> B).
proof: Proof. intros; assumption. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.CoreTactics Equations.Signature Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec