fact: Definition NULL {_34091 : Type'} := @ε ((prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop) (fun NULL' : (prod nat (prod nat (prod nat nat))) -> (list _34091) -> Prop => forall _18129 : prod nat (prod nat (prod nat nat)), ((NULL' _18129 (@nil _34091)) = True) /\ (forall h : _34091, forall t : list _34091, (NULL' _18129 (@cons _34091 h t)) = False)) (@pair nat (prod nat (prod nat nat)) (NUMERAL (BIT0 (BIT1 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (@pair nat (prod nat nat) (NUMERAL (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 (BIT0 (BIT1 0)))))))) (@pair nat nat (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0)))))))) (NUMERAL (BIT0 (BIT0 (BIT1 (BIT1 (BIT0 (BIT0 (BIT1 0))))))))))).
imports: coq theory_hol types