proposition: Lemma CONS_def {A : Type'} : (@cons A) = (fun a0 : A => fun a1 : list A => @_mk_list A ((fun a0' : A => fun a1' : recspace A => @CONSTR A (S (NUMERAL 0)) a0' (@FCONS (recspace A) a1' (fun n : nat => @BOTTOM A))) a0 (@_dest_list A a1))).
proof: Proof. apply fun_ext. intro a. apply fun_ext; intro l. 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 (cons a l). 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