Skip to content

Instantly share code, notes, and snippets.

@lf94

lf94/andb_eq_orb.v

Created August 9, 2020 22:28
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save lf94/e3247b3487b85b1f518f80298b108bc4 to your computer and use it in GitHub Desktop.
Save lf94/e3247b3487b85b1f518f80298b108bc4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
andb_eq_orb.v
Theorem andb_eq_orb :
forall (b c : bool),
(andb b c = orb b c) ->
b = c.
Proof.
intros b c.
destruct b eqn:Eb.
- destruct c eqn:Ec.
+ reflexivity.
+ simpl. rewrite <- Eb. intros H. rewrite -> H. reflexivity.
- destruct c eqn:Ec.
+ simpl. rewrite <- Eb. intros H. rewrite -> H. reflexivity.
+ reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment