Definition EqN := R (.\"EqN", "n", "m"; "n" ("m" true false_1) (.\"n"; "m" false (.\"m"; "EqN" "n" "m"))).

Lemma EqN_rec_00 : EqN (enc 0) (enc 0) == true.

Lemma EqN_rec_0S n : EqN (enc 0) (enc (S n)) == false.

Lemma EqN_rec_S0 n : EqN (enc (S n)) (enc 0) == false.

Lemma EqN_rec_SS n m : EqN (enc (S n)) (enc (S m)) == EqN (enc n) (enc m) .

Lemma EqN_correct m n : m = n ∧ EqN (enc m) (enc n) == true ∨ m ≠ n ∧ EqN (enc m) (enc n) == false.

Definition Eq := R (.\ "Eq", "s", "t"; "s" (.\"n"; "t" (.\"m"; !EqN "m" "n") false_2 false_1)
                                           (.\"s1", "s2"; "t" false_1 (.\"t1","t2"; !Andalso ("Eq" "s1" "t1") ("Eq" "s2" "t2")) false_1)
                                           (.\"s1"; "t" false_1 false_2 (.\"t1"; "Eq" "s1" "t1")) ).

Lemma Eq_correct_t s t :
      (s = t → Eq (tenc s) (tenc t) == true ).

Lemma Eq_correct_f s t :
  ( s ≠ t → Eq (tenc s) (tenc t) == false ).

Lemma Eq_correct s t :
      (s = t → Eq (tenc s) (tenc t) == true )
  ∧ ( s ≠ t → Eq (tenc s) (tenc t) == false ).