require import AllCore.

(* rewriting can also be used with non-equational formulas *)

lemma foo (a b : bool) :
  a => b => (a /\ b) \/ (!a /\ b).
proof.
move => a_true b_true.
rewrite a_true b_true //.  (* // in rewriting is also trivial *)
qed.

lemma goo (a b : bool) :
  ! a => b => (a /\ b) \/ (!a /\ b).
proof.
move => a_false b_true.
by rewrite a_false b_true.
qed.

lemma foo' (a b : bool) :
  a => b => (a /\ b) \/ (!a /\ b).
proof.
move => -> -> //.
qed.

lemma goo' (a b : bool) :
  ! a => b => (a /\ b) \/ (!a /\ b).
proof.
move => -> -> //.
qed.