proposition: Lemma demo_case_if : forall b c :bool, (if b then true else true) = false -> (if c then true else true) = true.
proof: Proof. Proof using. intros. dup 4. case_if. auto. auto. case_if as P. auto. auto. case_if in H. case_if in H as P. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia