proposition: Lemma COND_list {A : Type'} (l0 l1 l2 : list A) : match l0 with | nil => l1 | cons h t => l2 end = COND (l0 = nil) l1 l2.
proof: Proof. induction l0. symmetry. assert ((@nil A = nil) = True). apply prop_ext. auto. auto. rewrite H. apply COND_True. assert ((a :: l0 = nil) = False). apply prop_ext. intro. assert (nil <> a :: l0). apply nil_cons. easy. easy. rewrite H. symmetry. apply COND_False. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List