proposition: Lemma app_cons_eq_nil A (l1 l2 : list A) a : l1 ++ a :: l2 = nil <-> False.
proof: Proof. destruct l1; ins; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation