An error message generated by Aya (fuel = 2)

aya-error-message.txt

C:\Java\LibericaJDK-19\bin\java.exe --enable-preview ... -m aya.cli.console/org.aya.cli.console.Main test.aya --pretty-dir=out --pretty-stage=typed --pretty-format=html
In file test.aya:116:4 ->

  114 │   | Γ ▷ A => Sig (Γw : WfCon Γ) ** (WfTy Γ Γw A)
  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
      │       ╰──╯

Error: Unhandled case:
         Γ, _5, {Γ'}, Subst U ε
         Γ, _5, {Γ'}, Subst U (... ∘)
         Γ, _5, {Γ'}, Subst U (π₁ ...)
         Γ, _5, {Γ'}, Subst U (id ...)
         Γ, _5, {Γ'}, Subst U (idl• ...)
         Γ, _5, {Γ'}, Subst U (idr• ...)
         Γ, _5, {Γ'}, Subst U (ass ...)
         Γ, _5, {Γ'}, Subst U (π₁β ...)
         Γ, _5, {Γ'}, Subst U (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (Π ...) ε
         Γ, _5, {Γ'}, Subst (Π ...) (... ∘)
         Γ, _5, {Γ'}, Subst (Π ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (Π ...) (id ...)
         Γ, _5, {Γ'}, Subst (Π ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (Π ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (Π ...) (ass ...)
         Γ, _5, {Γ'}, Subst (Π ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (Π ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (El' ...) ε
         Γ, _5, {Γ'}, Subst (El' ...) (... ∘)
         Γ, _5, {Γ'}, Subst (El' ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (El' ...) (id ...)
         Γ, _5, {Γ'}, Subst (El' ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (El' ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (El' ...) (ass ...)
         Γ, _5, {Γ'}, Subst (El' ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (El' ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (Subst ...) ε
         Γ, _5, {Γ'}, Subst (Subst ...) (... ∘)
         Γ, _5, {Γ'}, Subst (Subst ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (id ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (ass ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubId ...) ε
         Γ, _5, {Γ'}, Subst (SubId ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubId ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) ε
         Γ, _5, {Γ'}, Subst (SubAss ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubAss ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubU ...) ε
         Γ, _5, {Γ'}, Subst (SubU ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubU ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) ε
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (... ∘)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (id ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (ass ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst U (... ∷)
         Γ, _5, {Γ'}, Subst U (... ∘)
         Γ, _5, {Γ'}, Subst U (π₁ ...)
         Γ, _5, {Γ'}, Subst U (id ...)
         Γ, _5, {Γ'}, Subst U (idl• ...)
         Γ, _5, {Γ'}, Subst U (idr• ...)
         Γ, _5, {Γ'}, Subst U (ass ...)
         Γ, _5, {Γ'}, Subst U (π₁β ...)
         Γ, _5, {Γ'}, Subst U (πη ...)
         Γ, _5, {Γ'}, Subst U (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (Π ...) (... ∷)
         Γ, _5, {Γ'}, Subst (Π ...) (... ∘)
         Γ, _5, {Γ'}, Subst (Π ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (Π ...) (id ...)
         Γ, _5, {Γ'}, Subst (Π ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (Π ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (Π ...) (ass ...)
         Γ, _5, {Γ'}, Subst (Π ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (Π ...) (πη ...)
         Γ, _5, {Γ'}, Subst (Π ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (El' ...) (... ∷)
         Γ, _5, {Γ'}, Subst (El' ...) (... ∘)
         Γ, _5, {Γ'}, Subst (El' ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (El' ...) (id ...)
         Γ, _5, {Γ'}, Subst (El' ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (El' ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (El' ...) (ass ...)
         Γ, _5, {Γ'}, Subst (El' ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (El' ...) (πη ...)
         Γ, _5, {Γ'}, Subst (El' ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (... ∷)
         Γ, _5, {Γ'}, Subst (Subst ...) (... ∘)
         Γ, _5, {Γ'}, Subst (Subst ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (id ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (ass ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (πη ...)
         Γ, _5, {Γ'}, Subst (Subst ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (... ∷)
         Γ, _5, {Γ'}, Subst (SubId ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubId ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (πη ...)
         Γ, _5, {Γ'}, Subst (SubId ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (... ∷)
         Γ, _5, {Γ'}, Subst (SubAss ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubAss ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (πη ...)
         Γ, _5, {Γ'}, Subst (SubAss ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (... ∷)
         Γ, _5, {Γ'}, Subst (SubU ...) (... ∘)
         Γ, _5, {Γ'}, Subst (SubU ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (id ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (ass ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (πη ...)
         Γ, _5, {Γ'}, Subst (SubU ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (... ∷)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (... ∘)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (π₁ ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (id ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (idl• ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (idr• ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (ass ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (π₁β ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (πη ...)
         Γ, _5, {Γ'}, Subst (TyTrunc ...) (TmsTrunc ...)
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubId i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε ε i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss ε (... ∷) i
         Γ, _5, {Γ'}, SubAss ε (... ∘) i
         Γ, _5, {Γ'}, SubAss ε (π₁ ...) i
         Γ, _5, {Γ'}, SubAss ε (id ...) i
         Γ, _5, {Γ'}, SubAss ε (idl• ...) i
         Γ, _5, {Γ'}, SubAss ε (idr• ...) i
         Γ, _5, {Γ'}, SubAss ε (ass ...) i
         Γ, _5, {Γ'}, SubAss ε (π₁β ...) i
         Γ, _5, {Γ'}, SubAss ε (πη ...) i
         Γ, _5, {Γ'}, SubAss ε (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) ε i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) ε i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) ε i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) ε i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) ε i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) ε i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) ε i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) ε i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) ε i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∷) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∷) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∷) i
         Γ, _5, {Γ'}, SubAss (... ∘) (... ∘) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (id ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (ass ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (πη ...) i
         Γ, _5, {Γ'}, SubAss (... ∘) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁ ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (id ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (id ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idl• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (idr• ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (ass ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (ass ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (π₁β ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (πη ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (πη ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∷) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (... ∘) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁ ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (id ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idl• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (idr• ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (ass ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (π₁β ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (πη ...) i
         Γ, _5, {Γ'}, SubAss (TmsTrunc ...) (TmsTrunc ...) i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, SubU i
         Γ, _5, {Γ'}, TyTrunc U U a b i i
         Γ, _5, {Γ'}, TyTrunc U (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc U (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Π ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (El' ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (Subst ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubId ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubAss ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (SubU ...) (TyTrunc ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) U a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (Π ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (El' ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (Subst ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (SubId ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (SubAss ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (SubU ...) a b i i
         Γ, _5, {Γ'}, TyTrunc (TyTrunc ...) (TyTrunc ...) a b i i

In file test.aya:117:70 ->

  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
  117 │   | Γ, Γw, {Γ'}, Π A B => Sig (Γ = Γ') (Aw : WfTy Γ Γw A) ** (WfTy (Γ ▷ A) (Γw ▷ Aw) B)
      │                                                                         ╰╯

Error: Cannot check the expression
         A
       of type
         Ty Γ'
       against the type
         Ty Γ
       In particular, we failed to unify
         Γ'
       with
         Γ

In file test.aya:117:74 ->

  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
  117 │   | Γ, Γw, {Γ'}, Π A B => Sig (Γ = Γ') (Aw : WfTy Γ Γw A) ** (WfTy (Γ ▷ A) (Γw ▷ Aw) B)
      │                                                                             ╰╯

Error: Cannot check the expression
         Γw
       of type
         WfCon Γ
       against the type
         Con

In file test.aya:117:79 ->

  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
  117 │   | Γ, Γw, {Γ'}, Π A B => Sig (Γ = Γ') (Aw : WfTy Γ Γw A) ** (WfTy (Γ ▷ A) (Γw ▷ Aw) B)
      │                                                                                  ╰╯

Error: Cannot check the expression
         Aw
       of type
         WfTy Γ Γw A
       against the type
         Ty <Γw>

In file test.aya:117:74 ->

  115 │   
  116 │   def WfTy (Γ : Con) (WfCon Γ) {Γ' : Con} (Ty Γ') : Type
  117 │   | Γ, Γw, {Γ'}, Π A B => Sig (Γ = Γ') (Aw : WfTy Γ Γw A) ** (WfTy (Γ ▷ A) (Γw ▷ Aw) B)
      │                                                                             ╰─────╯

Error: Cannot check the expression
         Γw ▷ Aw
       of type
         Con
       against the type
         WfCon (Γ ▷ <A>)
         (Normalized: Σ (Γw : WfCon Γ) ** WfTy Γ Γw <A>)

5 error(s), 0 warning(s).
🔨

Process finished with exit code 1