proposition: Lemma inductively_barred_at_imp_is_path_from : forall P, demorgan_inductively_barred_at P -> forall n l, ~ inductively_barred_at P n l -> is_path_from P n l.
proof: Proof. intros P Hdemorgan; induction n; intros l H. - apply here. intro. apply H. apply now_at. auto. - assert (H0:~ (inductively_barred_at P n (true::l) /\ inductively_barred_at P n (false::l))) by firstorder using inductively_barred_at. assert (HnP:~ P l) by firstorder using inductively_barred_at. apply Hdemorgan in H0 as [H0|H0]; apply IHn in H0; auto using is_path_from. Qed.
imports: WeakFan List Arith Compare_dec