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