proposition: Lemma Y_unique : forall P l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.
proof: Proof. induction l1, l2. - trivial. - discriminate. - discriminate. - intros H (HY1,H1) (HY2,H2). injection H as [= H]. pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. subst l1. f_equal. destruct a, b; firstorder. Qed.
imports: List