proposition: Lemma EquivAssignables_ind_refl: forall p h a, EquivAssignables_ind p h h a a.
proof: Proof. intros. induction a. apply EquivAssignables_base;trivial. apply EquivAssignables_step with a a0 a a0;trivial. apply LocSet.eq_refl. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)