proposition: Lemma EquivAssignables_refl: forall p st, EquivAssignables p st st.
proof: Proof. intros. unfold EquivAssignables. unfold level. rewrite nat_compare_n_n. apply EquivAssignables_ind_refl. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)