proposition: Lemma Pi_equiv_list : forall pi v1 v2 l r, MDP.Pi pi v1 v2 r l <-> In (l,r) (Pi_as_list pi v1 v2).
proof: Proof. intros pi v1 v2 l r. split. inversion 1;subst;simpl;auto with *. inversion 1;subst. injection H0;intros;subst;constructor. inversion H0. injection H1;intros;subst;constructor. case H1. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)