fact: Definition le9 T0 T1 T2 T3 T4 T5 T6 T7 T8 (p q : rel9 T0 T1 T2 T3 T4 T5 T6 T7 T8) := (forall x0 x1 x2 x3 x4 x5 x6 x7 x8 (PR: p x0 x1 x2 x3 x4 x5 x6 x7 x8 : Prop), q x0 x1 x2 x3 x4 x5 x6 x7 x8 : Prop).
imports: Paco(paconotation)