proposition: Lemma is_transitive_closure_incl: ∀ (k : nat) (gs : list (graph k)) (g : graph k) (l acc l' : list (graph k)), is_transitive_closure gs l' → incl_transitive_closure_of gs ((g :: l) ++ acc) → incl_transitive_closure_of ((g :: l) ++ acc) l'.
proof: Proof. intros k gs g l acc l' H0 H3. red in H3. pose proof (H3 _ H0). red. intros. assert (is_transitive_closure (g :: l ++ acc) l'). red. intuition. red in H0. intuition. red in H1, H2 |- *. intuition. Admitted. Ltac apply_find_opt_spec := match goal with | |- context [find_opt ?g ?f] => pose proof (find_opt_spec g f) end. Lemma existsb_spec {A} (p : A -> bool) l : reflect (exists x, In x l /\ p x = true) (existsb p l). Proof. destruct existsb eqn:Heq. constructor. now apply existsb_exists in Heq. constructor. intro. apply existsb_exists in H. rewrite Heq in H; discriminate. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect