I have definition:
Definition f (b1 b2 : bool) :bool :=
match b1 with
| true => true
| false => b2
end.
And Lemma...
Lemma l1: forall p : bool, f p false = true.
What I have tried is this:
Lemma l1: forall p : bool, f p false = true.
Proof.
intros p.
destruct p.
simpl.
reflexivity.
simpl.
And then I get false=true. What to do?