Parameter Fast1 : forall A : CN, A -> Prop. Parameter FASTER_THAN : forall A : CN, {p : A -> A -> Prop & forall h1 h2 h3 : A, (p h1 h2 /\ p h2 h3 -> p h1 h3) /\ (forall h4 h5 : A, p h4 h5 -> Fast1 A h4 -> Fast1 A h5)}. Definition faster_than:= fun A:CN=>projT1 (FASTER_THAN A). Parameter Slow : forall A : CN, A -> Prop. Parameter SLOWER_THAN : forall A : CN, {p : A -> A -> Prop & forall h1 h2 h3 : A, (p h1 h2 /\ p h2 h3 -> p h1 h3) /\ (forall h4 h5 : A, p h4 h5 -> Slow A h4 -> Slow A h5)}. Definition slower_than:= fun A:CN=>projT1 (SLOWER_THAN A). Parameter PC6082 : Object. Parameter ITELXZ : Object. Variables o1 o2 o3 : Object. Definition slow :=fun (A : CN) (a : A) => Slow A a /\ ~ (Fast1 A a). Definition as_fast_as:= fun A:CN, fun a:A, fun b:A=> Fast1 A b ->Fast1 A a. Parameter SMALLER_THAN: forall A:CN, sigT(fun p:A->A->Prop=> forall h1:A,forall h2:A,forall h3:A, (p(h1)(h2)/\ p(h2)(h3)->p(h1)(h3))/\ forall h1 h2:A, p h1 h2 -> (Small A(h1)-> Small A(h2))). Parameter LARGER_THAN: forall A:CN, sigT(fun p:A->A->Prop=> forall h1:A,forall h2:A,forall h3:A, (p(h1)(h2)/\ p(h2)(h3)->p(h1)(h3))/\ forall h1 h2:A,p h1 h2 -> (Large A(h1)-> Large A(h2))). Definition smaller_than:= fun A:CN=>projT1 (SMALLER_THAN A). Definition larger_than:= fun A:CN=>projT1 (LARGER_THAN A). Definition small:= fun (A : CN) (a : A) => Small A a/\~ Large A a /\ ~ Normalsized A a /\ (forall x : A, Large A x \/ Normalsized A x -> smaller_than A x a/\ not(larger_than A x a)). Parameter Elephant:CN. Variables f1 f2 f3: Object. Axiom dsdfsd : Elephant -> Animal. Coercion dsdfsd:Elephant>->Animal. Parameter Jumbo : Elephant.