proposition: Lemma axiom_16' : forall {A : Type'} (r : recspace A), (list_pred r) = ((@_dest_list A (@_mk_list A r)) = r).
proof: Proof. intros A r. apply prop_ext. intro h. apply (@ε_spec _ (_mk_list_pred r)). rewrite list_eq in h. induction h. exists nil. reflexivity. exists (cons a'' l''). reflexivity. intro e. rewrite <- e. intros P h. apply h. destruct (_mk_list r). left. reflexivity. right. exists t0. exists (_dest_list l). split. reflexivity. apply h. generalize l. induction l0. left; reflexivity. right. exists a. exists (_dest_list l0). split. reflexivity. apply h. exact IHl0. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance