proposition: Lemma G_ext : G a I [=] G a J.
proof: Proof. intro t. apply iff_and. split. refl. cut (forall f, output_base (typ f) = a -> forall ts : Tes (arity (typ f)), t =>R* apps (Fun f) ts -> forall i (hi : Acc f i), int I (Vnth (inputs (typ f)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)) <-> int J (Vnth (inputs (typ f)) (Acc_arity hi)) (Vnth ts (Acc_arity hi))). intro h1. split. intros h2 f hf ts r i hi. rewrite <- h1; auto. intros h2 f hf ts r i hi. rewrite h1; auto. intros f hf ts r i hi. apply int_equiv. intros b h. apply e. destruct (Acc_ok h) as [j|[j1 j2]]. rewrite hf in j. intro k. absurd (b <B b). apply lt_antirefl. trans a; hyp. subst. apply lt_antirefl. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)