notation "ℱ\sub 1 x" non associative with precedence 60 for @{'F1 $x}.
notation > "ℱ_1" non associative with precedence 90 for @{F1 ???}.
notation "ℱ\sub 1 x" non associative with precedence 60 for @{'F1 $x}.
notation > "ℱ_1" non associative with precedence 90 for @{F1 ???}.
notation "ℱ\sub 2 x" non associative with precedence 60 for @{'F2 $x}.
notation > "ℱ_2" non associative with precedence 90 for @{F2 ???}.
notation "ℱ\sub 2 x" non associative with precedence 60 for @{'F2 $x}.
notation > "ℱ_2" non associative with precedence 90 for @{F2 ???}.
lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F.
arrows2 C2 (F (ℱ_1 X)) (F (ℱ_1 Y)) →
lemma REW : ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀X,Y:Fo ?? F.
arrows2 C2 (F (ℱ_1 X)) (F (ℱ_1 Y)) →
notation "ℳ\sub 1 x" non associative with precedence 60 for @{'Fm1 $x}.
notation > "ℳ_1" non associative with precedence 90 for @{Fm1 ?????}.
notation "ℳ\sub 1 x" non associative with precedence 60 for @{'Fm1 $x}.
notation > "ℳ_1" non associative with precedence 90 for @{Fm1 ?????}.
notation "ℳ\sub 2 x" non associative with precedence 60 for @{'Fm2 $x}.
notation > "ℳ_2" non associative with precedence 90 for @{Fm2 ?????}.
notation "ℳ\sub 2 x" non associative with precedence 60 for @{'Fm2 $x}.
notation > "ℳ_2" non associative with precedence 90 for @{Fm2 ?????}.