proposition: Lemma cont_eq_intro : forall f f', f = f' -> forall c c', c = c' -> forall i v1 i' v1' (h1 : i'=i) j v2 (e : i+S j=arity f) j' v2' (h2 : j'=j) (e' : i'+S j'=arity f'), v1 = Vcast v1' h1 -> v2 = Vcast v2' h2 -> Cont e v1 c v2 = Cont e' v1' c' v2'.
proof: Proof. intros f f' hf. subst f'. intros c c' hc. subst c'. destruct v1. destruct i'; intros v1' h1. 2: discr. VOtac. rewrite Vcast_refl. clear h1. destruct v2; intros; clear H; destruct j'; try discr. VOtac. assert (e'=e). apply eq_unique. subst e'. refl. inversion h2. subst j'. rewrite Vcast_refl in H0. rewrite <- H0. assert (e'=e). apply eq_unique. subst e'. refl. destruct i'; intros v1' h1. discr. inversion h1. subst i'. rewrite Vcast_refl. clear h1. destruct v2; destruct j'; try discr; intros; rewrite <- H; clear H. VOtac. assert (e'=e). apply eq_unique. subst e'. refl. inversion h2. subst n0. rewrite Vcast_refl in H0. rewrite <- H0. assert (e'=e). apply eq_unique. subst e'. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)