proposition: Theorem inductive_invariant_true_in_reachable : forall step init P, inductive_invariant step init P -> true_in_reachable step init P.
proof: Proof. Proof using. unfold inductive_invariant, true_in_reachable, reachable, inductive in *. intros. break_exists. match goal with H : refl_trans_1n_trace _ _ _ _ |- _ => induction H end; intuition eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)