Library Bool
Require Export Tactics.
Definition true := .\"t", "f"; "t".
Definition false := .\"t", "f"; "f".
Definition Andalso : term := .\"a", "b"; "a" "b" false.
Definition Not : term := .\"a"; "a" false true.
Definition false_1 := .\"x" ; false.
Definition false_2 := .\"x", "x"; false.
Hint Unfold true false not false_1 false_2 Andalso : cbv.
Lemma Andalso_rec_tt : Andalso true true == true.
Proof. crush. Qed.
Lemma Andalso_rec_tf : Andalso true false == false.
Proof. crush. Qed.
Lemma Andalso_rec_ft : Andalso false true == false.
Proof. crush. Qed.
Lemma Andalso_rec_ff : Andalso false false == false.
Proof. crush. Qed.
Lemma not_rec_true : Not true == false.
Proof. crush. Qed.
Lemma not_rec_false : Not false == true.
Proof. crush. Qed.
Lemma true_equiv_false : ~ true == false.
Proof.
cbv. intros H. eapply eq_lam in H. inv H.
Qed.
Definition Orelse : term := .\"a", "b"; "a" true "b".
Hint Unfold Orelse : cbv.
Lemma Orelse_rec_tt : Orelse true true == true.
Proof. crush. Qed.
Lemma Orelse_rec_tf : Orelse true false == true.
Proof. crush. Qed.
Lemma Orelse_rec_ft : Orelse false true == true.
Proof. crush. Qed.
Lemma Orelse_rec_ff : Orelse false false == false.
Proof. crush. Qed.