proposition: Lemma EquivAssignables_ind_trans: forall p h h' h'' a a' a'', length a = length a' -> EquivAssignables_ind p h h' a a' -> length a' = length a'' -> EquivAssignables_ind p h' h'' a' a'' -> EquivAssignables_ind p h h'' a a''.
proof: Proof. intros p h h' h''. induction a. destruct a'. simpl in |- *. destruct a''. simpl in |- *. intros. apply EquivAssignables_base; trivial. intros. discriminate H1. intros. discriminate H. destruct a'. intros. discriminate H. destruct a''. intros. discriminate H1. intros. apply EquivAssignables_step with a a0 p1 a''; trivial. rewrite H1 in H. auto. apply IHa with a'. auto. apply EquivAssignables_ind_tail with a p0. auto. trivial. auto. apply EquivAssignables_ind_tail with p0 p1. auto. trivial. destruct H0. discriminate H0. destruct H2. discriminate H2. inversion H0. inversion H3. inversion H2. inversion H7. subst. inversion H2. subst. generalize H10. generalize H6. apply LocSet.eq_trans. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)