proposition: Lemma demo_fequals_1 : forall a b c d, b = d -> d = 2 -> a = 1 -> (a,b,c) = (1,2,3).
proof: Proof. Proof using. intros. dup 3. f_equal. f_equal. demo. demo. demo. fequal. demo. demo. demo. fequals. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia