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.

Lemma Andalso_rec_tt : Andalso true true == true.

Lemma Andalso_rec_tf : Andalso true false == false.

Lemma Andalso_rec_ft : Andalso false true == false.

Lemma Andalso_rec_ff : Andalso false false == false.

Lemma not_rec_true : Not true == false.

Lemma not_rec_false : Not false == true.

Lemma true_equiv_false : ¬ true == false.

Definition Orelse : term := .\"a", "b"; "a" true "b".

Lemma Orelse_rec_tt : Orelse true true == true.

Lemma Orelse_rec_tf : Orelse true false == true.

Lemma Orelse_rec_ft : Orelse false true == true.

Lemma Orelse_rec_ff : Orelse false false == false.