A Lean Companion to Conceptual Mathematics

Test 5πŸ”—

Problem 1 (p. 301)

Find as many graphs with exactly 4 dots and 2 arrows as you can, with no two of your graphs isomorphic. (Draw an internal diagram of each of your graphs.)

def Example : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 2 toTgt := fun | 0 => 1 | 1 => 1 }

Hint: The number of such graphs is between 10 and 15.

Solution: Problem 1

There are 11 such graphsβ€”2 graphs with exactly 2 loops, 3 graphs with exactly one loop, and 6 graphs with no loops. We provide definitions below.

Graphs with exactly 2 loops:

def G₁ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 0 toTgt := fun | 0 => 0 | 1 => 0 } def Gβ‚‚ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 0 | 1 => 1 }

Graphs with exactly 1 loop:

def G₃ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 0 toTgt := fun | 0 => 0 | 1 => 1 } def Gβ‚„ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 0 | 1 => 0 } def Gβ‚… : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 0 | 1 => 2 }

Graphs with no loops:

def G₆ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 0 toTgt := fun | 0 => 1 | 1 => 1 } def G₇ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 1 | 1 => 2 } def Gβ‚ˆ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 2 toTgt := fun | 0 => 1 | 1 => 3 } def G₉ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 1 | 1 => 0 } def G₁₀ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 0 | 1 => 2 toTgt := fun | 0 => 1 | 1 => 1 } def G₁₁ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 4 toSrc := fun | 0 => 1 | 1 => 1 toTgt := fun | 0 => 0 | 1 => 2 }
Problem 2 (p. 301)abbrev IrreflexiveGraph.D : IrreflexiveGraph := { carrierA := Empty carrierD := Unit toSrc := Empty.elim toTgt := Empty.elim } abbrev IrreflexiveGraph.A : IrreflexiveGraph := { carrierA := Unit carrierD := Fin 2 toSrc := fun _ ↦ 0 toTgt := fun _ ↦ 1 } abbrev I : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 3 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 1 | 1 => 2 }

Find numbers a, b, c such that I \times I = aD + bA + cI Hint: First try to draw {I \times I}

To check your picture, be sure that the two projection maps are maps of graphs!

Solution: Problem 2

We can formalise {I \times I} as follows:

abbrev IxI : IrreflexiveGraph := { carrierA := Fin 4 carrierD := Fin 3 Γ— Fin 3 toSrc := fun | 0 => (0, 0) | 1 => (0, 1) | 2 => (1, 0) | 3 => (1, 1) toTgt := fun | 0 => (1, 1) | 1 => (1, 2) | 2 => (2, 1) | 3 => (2, 2) }

We then find that {I \times I} is isomorphic to the graph {2D + 2A + I}, which we can formalise using Lean's Sigma type (dependent pairs) as follows:

open IrreflexiveGraph abbrev Fam2D2AI : Fin 5 β†’ IrreflexiveGraph | 0 => D | 1 => D | 2 => A | 3 => A | 4 => I def G : IrreflexiveGraph := { carrierA := Ξ£ i, (Fam2D2AI i).carrierA carrierD := Ξ£ i, (Fam2D2AI i).carrierD toSrc := fun ⟨i, a⟩ ↦ ⟨i, (Fam2D2AI i).toSrc a⟩ toTgt := fun ⟨i, a⟩ ↦ ⟨i, (Fam2D2AI i).toTgt a⟩ }

We prove the isomorphism {I \times I \cong 2D + 2A + I} below.

example : IxI β‰… G := { hom := ⟨ (fun | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), ⊒ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toSrc = G.toSrc ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1 ∧ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt = G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1 ⊒ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toSrc = G.toSrc ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1⊒ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt = G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1 all_goals a:IxI.carrierA⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) a = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) a; ⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨1, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨2, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨2, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨3, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨3, β‹―βŸ©) ⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨0, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨0, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨1, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨1, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨2, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨2, β‹―βŸ©)⊒ ((fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).2 ⊚ IxI.toTgt) ((fun i ↦ i) ⟨3, β‹―βŸ©) = (G.toTgt ⊚ (fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩).1) ((fun i ↦ i) ⟨3, β‹―βŸ©) All goals completed! πŸ™ ⟩ inv := ⟨ (fun | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, ()⟩ => 1 | ⟨3, ()⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun | ⟨0, ()⟩ => (0, 2) | ⟨1, ()⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), ⊒ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toSrc = IxI.toSrc ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1 ∧ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt = IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1 ⊒ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toSrc = IxI.toSrc ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1⊒ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt = IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1 all_goals i:Fin 5a:(Fam2D2AI i).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨i, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨i, a⟩ a:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ a:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierA⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ ⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© ⊒ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ ((fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).2 ⊚ G.toTgt) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (IxI.toTgt ⊚ (fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)).1) ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© All goals completed! πŸ™ ⟩ hom_inv_id := ⊒ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© = πŸ™ IxI ⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).1 = (↑(πŸ™ IxI)).1⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 = (↑(πŸ™ IxI)).2 all_goals x:IxI.carrierD⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 x = (↑(πŸ™ IxI)).2 x; ⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) ⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨0, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨1, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©)⊒ (↑(⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ©)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) = (↑(πŸ™ IxI)).2 ((fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©) All goals completed! πŸ™ inv_hom_id := ⊒ ⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ© = πŸ™ G ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 = (↑(πŸ™ G)).1⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 = (↑(πŸ™ G)).2 ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 = (↑(πŸ™ G)).1 i:Fin 5a:(Fam2D2AI i).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨i, a⟩ = (↑(πŸ™ G)).1 ⟨i, a⟩ a:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩a:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ a:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, a⟩ All goals completed! πŸ™ a:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierA⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, a⟩ ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).1 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© All goals completed! πŸ™ ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 = (↑(πŸ™ G)).2 i:Fin 5d:(Fam2D2AI i).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨i, d⟩ = (↑(πŸ™ G)).2 ⟨i, d⟩ d:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, d⟩d:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, d⟩d:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, d⟩d:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, d⟩d:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, d⟩ d:(Fam2D2AI ((fun i ↦ i) ⟨0, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨0, β‹―βŸ©, d⟩ All goals completed! πŸ™ d:(Fam2D2AI ((fun i ↦ i) ⟨1, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨1, β‹―βŸ©, d⟩ All goals completed! πŸ™ d:(Fam2D2AI ((fun i ↦ i) ⟨2, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, d⟩ ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨2, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© All goals completed! πŸ™ d:(Fam2D2AI ((fun i ↦ i) ⟨3, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, d⟩ ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨3, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© All goals completed! πŸ™ d:(Fam2D2AI ((fun i ↦ i) ⟨4, β‹―βŸ©)).carrierD⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, d⟩ = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, d⟩ ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©βŸ© ⊒ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨0, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨1, β‹―βŸ©βŸ©βŠ’ (↑(⟨(fun x ↦ match x with | 0 => ⟨4, 0⟩ | 1 => ⟨2, ()⟩ | 2 => ⟨3, ()⟩ | 3 => ⟨4, 1⟩, fun x ↦ match x with | (0, 0) => ⟨4, 0⟩ | (0, 1) => ⟨2, 0⟩ | (0, 2) => ⟨0, ()⟩ | (1, 0) => ⟨3, 0⟩ | (1, 1) => ⟨4, 1⟩ | (1, 2) => ⟨2, 1⟩ | (2, 0) => ⟨1, ()⟩ | (2, 1) => ⟨3, 1⟩ | (2, 2) => ⟨4, 2⟩), β‹―βŸ© ⊚ ⟨(fun x ↦ match x with | ⟨0, a⟩ => nomatch a | ⟨1, a⟩ => nomatch a | ⟨2, PUnit.unit⟩ => 1 | ⟨3, PUnit.unit⟩ => 2 | ⟨4, 0⟩ => 0 | ⟨4, 1⟩ => 3, fun x ↦ match x with | ⟨0, PUnit.unit⟩ => (0, 2) | ⟨1, PUnit.unit⟩ => (2, 0) | ⟨2, 0⟩ => (0, 1) | ⟨2, 1⟩ => (1, 2) | ⟨3, 0⟩ => (1, 0) | ⟨3, 1⟩ => (2, 1) | ⟨4, 0⟩ => (0, 0) | ⟨4, 1⟩ => (1, 1) | ⟨4, 2⟩ => (2, 2)), β‹―βŸ©)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©βŸ© = (↑(πŸ™ G)).2 ⟨(fun i ↦ i) ⟨4, β‹―βŸ©, (fun i ↦ i) ⟨2, β‹―βŸ©βŸ© All goals completed! πŸ™ }