require import AllCore.

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

lemma foo (a b : bool) :
  a => b => (a /\ b) \/ (!a /\ b).
proof.

qed.

lemma goo (a b : bool) :
  ! a => b => (a /\ b) \/ (!a /\ b).
proof.

qed.

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

qed.

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

qed.