proposition: Lemma NULL_def {_34091 : Type'} : (@NULL _34091) = (@ε ((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)))))))))))).
proof: Proof. exact (eq_refl (@NULL _34091)). Qed.
imports: coq theory_hol types