proposition: Lemma find_left_path : forall P l n, is_path_from P (S n) l -> inductively_barred_at P n (false :: l) -> is_path_from P n (true :: l).
proof: Proof. inversion 1; subst; intros. - auto. - exfalso. eauto using is_path_from_imp_inductively_barred_at. Qed.
imports: WeakFan List Arith Compare_dec