proposition: Lemma EquivAssignables_ind_tail: forall p h h' a t a' t', length t = length t' -> EquivAssignables_ind p h h' (a::t) (a'::t') -> EquivAssignables_ind p h h' t t'.
proof: Proof. intros. replace t with (pop (a :: t)) by trivial. replace t' with (pop (a' :: t')) by trivial. rewrite <- truncate_pop with (LocSet.t * LocSet.t)%type (length t ) (a :: t). rewrite <- truncate_pop with (LocSet.t * LocSet.t)%type (length t' ) (a' :: t'). rewrite <- H. apply EquivAssignables_ind_truncated. simpl; auto. trivial. trivial. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)