proposition: Lemma demo_introv_3 : forall a, a = 0 -> Sym a.
proof: Proof. Proof using. dup 5. introv. demo. introv E. demo. introv E F. demo. introv E F G. demo. try (introv E F G H). demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia