proposition: Lemma _dest_list_inj : forall {A : Type'} (l l' : list A), _dest_list l = _dest_list l' -> l = l'.
proof: Proof. induction l; induction l'; simpl; rewrite (@CONSTR_INJ A); intros [e1 [e2 e3]]. reflexivity. discriminate. discriminate. rewrite e2. rewrite (@IHl l'). reflexivity. rewrite <- (FCONS_0 (_dest_list l) ((fun _ : nat => BOTTOM))). rewrite <- (FCONS_0 (_dest_list l') ((fun _ : nat => BOTTOM))). rewrite e3. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance