proposition: Lemma list_eq {A : Type'} : @list_pred A = @list_ind A.
proof: Proof. apply fun_ext. intro r. apply prop_ext. intro h. apply h. intros r' H. destruct H. rewrite H. exact list_ind0. destruct H. destruct H. destruct H. rewrite H. destruct H0. assert (_dest_list nil = @CONSTR A (NUMERAL 0) (@ε A (fun v : A => True)) (fun n : nat => @BOTTOM A)). reflexivity. rewrite <- H0. exact (list_ind1 x nil). assert (_dest_list (cons a'' l'') = @CONSTR A (S (NUMERAL 0)) a'' (@FCONS (recspace A) (@_dest_list A l'') (fun n : nat => @BOTTOM A))). reflexivity. rewrite <- H0. exact (list_ind1 x (a'':: l'')). induction 1; unfold list_pred; intros R h; apply h. left; reflexivity. right. exists a''. exists (_dest_list l''). split. reflexivity. apply h. induction l''. auto. right. exists a. exists (_dest_list l''). split. reflexivity. apply h. exact IHl''. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance