proposition: Lemma MethodReturnAction_Equiv: forall p st st_c st_c', st_c' = MethodReturnAction p st_c st -> EquivAssignables p st_c st_c'.
proof: Proof. intros. subst. unfold MethodReturnAction. unfold EquivAssignables. simpl. unfold pop. case_eq (st_c@fr@assignables). intro. simpl. apply EquivAssignables_ind_refl. intros. unfold level. replace (length (p0::l)) with (S (length l)) by auto. rewrite nat_compare_Sn_n. rewrite truncate_pop by auto. simpl. apply EquivAssignables_ind_refl. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)