proposition: Lemma EquivAssignables_ind_truncated: forall p h h' a a' n, length a = length a' -> EquivAssignables_ind p h h' a a' -> EquivAssignables_ind p h h' (truncate n a) (truncate n a').
proof: Proof. intros. induction H0. subst. apply EquivAssignables_base. unfold truncate in |- *. destruct Nat.compare; trivial. unfold truncate in |- *. destruct Nat.compare; trivial. apply IHEquivAssignables_ind in H2. subst. case_eq (Nat.compare n (length (head::tail))). intros. unfold truncate. rewrite H0. rewrite H in H0. rewrite H0. apply EquivAssignables_step with head tail head' tail';auto. intro. unfold truncate in |- *. rewrite H0 in |- *. rewrite H in H0. rewrite H0 in |- *. apply IHEquivAssignables_ind. progress auto. intro. unfold truncate in |- *. rewrite H0 in |- *. rewrite H in H0. rewrite H0 in |- *. apply EquivAssignables_step with head tail head' tail'; auto. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)