proposition: Lemma pi_reg : forall pi v0 v1 s t (H : MDP.Pi pi v0 v1 s t) x, In x (E.T.var_list s) -> In x (E.T.var_list t).
proof: Proof. intros pi v0 v1 s t H x H0. inversion H;subst;simpl in H0|-*. destruct H0;auto with *. destruct H0;auto with *. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)