proposition: Lemma Y_unique : forall P, demorgan_inductively_barred_at P -> forall l1 l2, length l1 = length l2 -> Y P l1 -> Y P l2 -> l1 = l2.
proof: Proof. intros * DeMorgan. induction l1, l2. - trivial. - discriminate. - discriminate. - intros [= H] (HY1,H1) (HY2,H2). pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. subst l1. f_equal. destruct a, b; try reflexivity. + destruct H1 as (n,Hbar). destruct (is_path_from_imp_inductively_barred_at _ _ _ (H2 n) Hbar). + destruct H2 as (n,Hbar). destruct (is_path_from_imp_inductively_barred_at _ _ _ (H1 n) Hbar). Qed.
imports: WeakFan List Arith Compare_dec