proposition: Lemma EquivAssignables_ind_sym: forall p h h' a a', EquivAssignables_ind p h h' a a' -> EquivAssignables_ind p h' h a' a.
proof: Proof. intros. induction H. subst. apply EquivAssignables_base;trivial. apply EquivAssignables_step with head' tail' head tail;trivial. symmetry;trivial. apply LocSet.eq_sym. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)