proposition: Lemma NUMPAIR_def : NUMPAIR = (fun _17487 : nat => fun _17488 : nat => Nat.mul (Nat.pow (NUMERAL (BIT0 (BIT1 0))) _17487) (Nat.add (Nat.mul (NUMERAL (BIT0 (BIT1 0))) _17488) (NUMERAL (BIT1 0)))).
proof: Proof. exact (eq_refl NUMPAIR). Qed.
imports: coq theory_hol types