proposition: Lemma NIL_def {A : Type'} : (@nil A) = (@_mk_list A (@CONSTR A (NUMERAL 0) (@ε A (fun v : A => True)) (fun n : nat => @BOTTOM A))).
proof: Proof. apply _dest_list_inj. simpl. match goal with [|- ?x = _] => set (r := x) end. unfold _mk_list. assert (h: exists l, @_mk_list_pred A r l). exists nil. reflexivity. generalize (ε_spec h). set (l := ε (_mk_list_pred r)). unfold _mk_list_pred. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance