proposition: Lemma EquivAssignables_ind_1: forall p h h' a a', EquivAssignables_ind p h h' a a' -> (forall n, UnfoldDatagroups_rac p h (fst (nth n a (LocSet.empty,LocSet.empty))) (snd (nth n a (LocSet.empty,LocSet.empty))) [=] UnfoldDatagroups_rac p h' (fst (nth n a' (LocSet.empty,LocSet.empty))) (snd (nth n a' (LocSet.empty,LocSet.empty)))).
proof: Proof. intros. generalize n. clear n. induction H. subst. simpl. destruct n; split; rewrite UnfoldDatagroups_rac_def; simpl; intros; destruct H as (dg, H); destruct H; elim LocSet_empty with dg; trivial. subst. destruct n. simpl. trivial. simpl. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)