proposition: Lemma demo_dependent_invert : behave 4 (Behave_intro (fun x:nat => x) (fun x:nat => x <> 3)) -> False.
proof: Proof. Proof using. intros H. dup 3. inversion H. demo. inverts H. demo. inverts H as R1 R2 R3. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia