put trace info in .out files

1 files changed, 299 insertions, 1 deletions

diff --git a/testdata/scope01.reject.out b/testdata/scope01.reject.out
index ef19f761..cd81041a 100644
--- a/testdata/scope01.reject.out
+++ b/testdata/scope01.reject.out
@@ -1,3 +1,301 @@
 can't find: frame' in testdata/scope01.reject.lc:3:18:
     in ScreenOut frame'
-                 ^^^^^^
\ No newline at end of file
+                 ^^^^^^
+------------ trace
+infer:  labelend (\(a := FrameBuffer (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := FrameBuffer (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := FrameBuffer (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := FrameBuffer (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {_ : _:'Type} (colorImage1 1.0)) -> ScreenOut frame')
+check:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) :: 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(i : _:'Type)->i : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:'Type -> i))->j : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:Type -> i))->j : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> j : 'List 'ImageSemantics} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> \(k : 'List 'ImageSemantics ~ i)->j} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> \(i := 'List 'ImageSemantics)->j} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i (i := 'List 'ImageSemantics) -> \(j : 'List 'ImageSemantics)->j} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:Type c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(i : 'List 'ImageSemantics)->i} (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type i:Type -> FrameBuffer c d e f g h i) {b}) (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {_ : _:'Type} (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) :: Type} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) : Type} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(i : _:'Type)->i : Type} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:'Type -> i))->j : Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:Type -> i))->j : Type} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : Type} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> j:Type} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> \(k : Type~i)->j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i i:=Type -> j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i i:=Type -> \j->j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c:Type d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c -> (\d:Type e:Type f:Type g:Type h:Type i:Type -> FrameBuffer b d e f g h i) {c}) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) -> (\c d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {_ : _:'Type} (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) :: 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(i : _:'Type)->i : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:'Type -> i))->j : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:Type -> i))->j : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> j:'Nat} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> \(k : 'Nat~i)->j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i i:='Nat -> j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i i:='Nat j:'Nat -> j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:Type e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i:'Nat -> i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:'Nat -> (\e:Type f:Type g:Type h:Type i:Type -> FrameBuffer b c e f g h i) {d}) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c -> (\d:'Nat e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {_ : _:'Type} (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) :: 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(_ : _:'Type) : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(i : _:'Type)->i : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:'Type -> i))->j : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : (\i:Type -> i))->j : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\(j : \i->i)->j : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {(\i j:i -> j) : 'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> j:'Unit} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i -> \(k : 'Unit~i)->j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i j:i i:='Unit -> j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i i:='Unit j:'Unit -> j} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {\i i:='Unit -> TT} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type h:Type -> FrameBuffer b c d e f g h) {TT} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {_ : _:'Type} (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {(_ : _:'Type) :: 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {(_ : _:'Type) : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(h : _:'Type)->h : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : (\h:'Type -> h))->i : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : (\h:Type -> h))->i : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : \h->h)->i : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : \h->h)->i : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> i : 'SameLayerCounts c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> \(j : 'SameLayerCounts c ~ h)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> \(h := 'SameLayerCounts c)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\h (h := 'SameLayerCounts c) -> \(i : 'SameLayerCounts c)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\e:Type f:Type g:Type -> FrameBuffer b c d TT e f g) {\(h : 'SameLayerCounts c)->h} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\(e : 'SameLayerCounts c) -> (\f:Type g:Type h:Type -> FrameBuffer b c d TT f g h) {e}) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat -> (\(e : 'SameLayerCounts c) f:Type g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {_ : _:'Type} (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {(_ : _:'Type) :: 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {(_ : _:'Type) : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(h : _:'Type)->h : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : (\h:'Type -> h))->i : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : (\h:Type -> h))->i : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : \h->h)->i : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(i : \h->h)->i : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {(\h i:h -> i) : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> i : 'FrameBuffer d b ~ 'TFFrameBuffer c} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> \(j : ('FrameBuffer d b ~ 'TFFrameBuffer c) ~ h)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\h i:h -> \(h := 'FrameBuffer d b ~ 'TFFrameBuffer c)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\h (h := 'FrameBuffer d b ~ 'TFFrameBuffer c) -> \(i : 'FrameBuffer d b ~ 'TFFrameBuffer c)->i} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\f:Type g:Type -> FrameBuffer b c d TT e f g) {\(h : 'FrameBuffer d b ~ 'TFFrameBuffer c)->h} (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\(f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type h:Type -> FrameBuffer b c d TT e g h) {f}) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) -> (\(f : 'FrameBuffer d b ~ 'TFFrameBuffer c) g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0 :: c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (colorImage1 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {_ : _:'Type} 1.0 : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) :: 'Nat} 1.0 : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) : 'Nat} 1.0 : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : _:'Type)->n : 'Nat} 1.0 : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:'Type -> n))->o : 'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:Type -> n))->o : 'Nat} 1.0 : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : 'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : 'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Nat} 1.0 : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> o:'Nat} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(p : 'Nat~n)->o} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n n:='Nat -> o} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n n:='Nat o:'Nat -> o} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:Type i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n:'Nat -> n} 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type n:Type -> ColorImage 1 i j k l m n) {h}) 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {_ : _:'Type} 1.0) : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) :: Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : _:'Type)->n : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:'Type -> n))->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:Type -> n))->o : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> o:Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(p : Type~n)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n n:=Type -> o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n n:=Type -> \o->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i:Type j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n->n} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i -> (\j:Type k:Type l:Type m:Type n:Type -> ColorImage 1 h j k l m n) {i}) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat -> (\i j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {_ : _:'Type} 1.0) : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) :: Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : _:'Type)->n : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:'Type -> n))->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:Type -> n))->o : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> o:Type} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(p : Type~n)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n n:=Type -> o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n n:=Type -> \o->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j:Type k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n->n} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j -> (\k:Type l:Type m:Type n:Type -> ColorImage 1 h i k l m n) {j}) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i -> (\j k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {_ : _:'Type} 1.0) : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) :: 'Num i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) : 'Num i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : _:'Type)->n : 'Num i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:'Type -> n))->o : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:Type -> n))->o : 'Num i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Num i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> o : 'Num i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(p : 'Num i ~ n)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(n := 'Num i)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\n (n := 'Num i) -> \(o : 'Num i)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\k:Type l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : 'Num i)->n} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\(k : 'Num i) -> (\l:Type m:Type n:Type -> ColorImage 1 h i j l m n) {k}) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j -> (\(k : 'Num i) l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {_ : _:'Type} 1.0) : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) :: j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {(_ : _:'Type) : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\(n : _:'Type)->n : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:'Type -> n))->o : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : (\n:Type -> n))->o : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\(o : \n->n)->o : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {(\n o:n -> o) : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> o : j ~ 'VecScalar h i} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(p : (j ~ 'VecScalar h i) ~ n)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\n o:n -> \(n := j ~ 'VecScalar h i)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\n (n := j ~ 'VecScalar h i) -> \(o : j ~ 'VecScalar h i)->o} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\l:Type m:Type -> ColorImage 1 h i j k l m) {\n (n := j ~ 'VecScalar h i) -> \(j := 'VecScalar h i)->TT} 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\(j := 'VecScalar h i) -> (\l:Type m:Type -> ColorImage 1 h i ('VecScalar h i) k l m) {TT}) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) -> (\(j := 'VecScalar h i) l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) 1.0) : c))) -> ScreenOut frame')
+check:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (1.0 :: 'VecScalar h i)) : c))) -> ScreenOut frame')
+infer:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (1.0 : 'VecScalar h i)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (1.0 : 'VecScalar h i)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) \(m : 'T2 h~1 i~'Float)->1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (\(m : h~1) -> \(n : i~'Float)->1.0)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (\(m : h~1) i:='Float -> 1.0)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (\i:='Float -> \(m : h~1)->1.0)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) -> (\l:Type -> ColorImage 1 h i ('VecScalar h i) k TT l) (\i:='Float h:=1 -> 1.0)) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) i:='Float h:=1 -> (\l:Type -> ColorImage 1 1 'Float 'Float k TT l) 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (k : 'Num i) (j := 'VecScalar h i) i:='Float h:=1 -> ColorImage 1 1 'Float 'Float k TT 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (j := 'VecScalar h i) i:='Float h:=1 k:'Unit -> ColorImage 1 1 'Float 'Float k TT 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) ((\h:'Nat i j (j := 'VecScalar h i) i:='Float h:=1 -> ColorImage 1 1 'Float 'Float TT TT 1.0) : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (ColorImage 1 1 'Float 'Float TT TT 1.0 : c))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (\(h : c ~ 'Image 1 (Color 'Float)) -> ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) -> (\g:Type -> FrameBuffer b c d TT e f g) (\(c := 'Image 1 (Color 'Float)) -> ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) (c := 'Image 1 (Color 'Float)) -> (\g:Type -> FrameBuffer b ('Image 1 (Color 'Float)) d TT e f g) (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (f : 'FrameBuffer d b ~ 'TFFrameBuffer c) (c := 'Image 1 (Color 'Float)) -> FrameBuffer b ('Image 1 (Color 'Float)) d TT e f (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) (f : 'T2 d~1 (b ~ Cons (Color 'Float) Nil)) -> FrameBuffer b ('Image 1 (Color 'Float)) d TT e f (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) (f : d~1) (g : b ~ Cons (Color 'Float) Nil) -> FrameBuffer b ('Image 1 (Color 'Float)) d TT e (t2C f g) (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) (f : d~1) (b := Cons (Color 'Float) Nil) -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) d TT e (t2C f TT) (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) (b := Cons (Color 'Float) Nil) (f : d~1) -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) d TT e (t2C f TT) (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) (b := Cons (Color 'Float) Nil) d:=1 -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT e TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\(b : 'List 'ImageSemantics) c d:'Nat (e : 'SameLayerCounts c) (c := 'Image 1 (Color 'Float)) d:=1 (b := Cons (Color 'Float) Nil) -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT e TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b c:'Nat (d : 'SameLayerCounts b) (b := 'Image 1 (Color 'Float)) c:=1 -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT d TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b c:'Nat (d : 'SameLayerCounts b) c:=1 (b := 'Image 1 (Color 'Float)) -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT d TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b c:'Nat c:=1 (b := 'Image 1 (Color 'Float)) d:'Unit -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT d TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b c:'Nat c:=1 (b := 'Image 1 (Color 'Float)) -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := (\b:'Nat b:=1 -> FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0))) -> ScreenOut frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {_ : _:'Type} frame')
+check:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {(_ : _:'Type) :: 'Nat} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {(_ : _:'Type) : 'Nat} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\(b : _:'Type)->b : 'Nat} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\(c : (\b:'Type -> b))->c : 'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\(c : (\b:Type -> b))->c : 'Nat} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\(c : \b->b)->c : 'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\(c : \b->b)->c : 'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {(\b c:b -> c) : 'Nat} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {(\b c:b -> c) : 'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {(\b c:b -> c) : 'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\b c:b -> c:'Nat} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\b c:b -> \(d : 'Nat~b)->c} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\b c:b b:='Nat -> c} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\b b:='Nat c:'Nat -> c} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> ScreenOut {\b:'Nat -> b} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> (\b:'Nat -> ScreenOut {b}) frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) -> (\b:'Nat -> ScreenOut b) frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {_ : _:'Type} frame')
+check:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {(_ : _:'Type) :: 'List 'ImageSemantics} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {(_ : _:'Type) : 'List 'ImageSemantics} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(c : _:'Type)->c : 'List 'ImageSemantics} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(d : (\c:'Type -> c))->d : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(d : (\c:Type -> c))->d : 'List 'ImageSemantics} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(d : \c->c)->d : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(d : \c->c)->d : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {(\c d:c -> d) : 'List 'ImageSemantics} frame')
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {(\c d:c -> d) : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {(\c d:c -> d) : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\c d:c -> d : 'List 'ImageSemantics} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\c d:c -> \(e : 'List 'ImageSemantics ~ c)->d} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\c d:c -> \(c := 'List 'ImageSemantics)->d} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\c (c := 'List 'ImageSemantics) -> \(d : 'List 'ImageSemantics)->d} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> ScreenOut b {\(c : 'List 'ImageSemantics)->c} frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> (\(c : 'List 'ImageSemantics) -> ScreenOut b {c}) frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat -> (\(c : 'List 'ImageSemantics) -> ScreenOut b c) frame')
+focus:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat (c : 'List 'ImageSemantics) -> ScreenOut b c frame')
+check:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat (c : 'List 'ImageSemantics) -> ScreenOut b c (frame' :: 'FrameBuffer b c))
+infer:  labEnd (\(a := FrameBuffer (Cons (Color 'Float) Nil) ('Image 1 (Color 'Float)) 1 TT TT TT (ColorImage 1 1 'Float 'Float TT TT 1.0)) b:'Nat (c : 'List 'ImageSemantics) -> ScreenOut b c (frame' : 'FrameBuffer b c))
+!can't find: frame' in testdata/scope01.reject.lc:3:18
+------------ tooltips
+testdata/scope01.reject.lc 2:17-2:28  {a : List ImageSemantics} -> {b} -> {c:Nat} -> {d:Unit} -> {e : SameLayerCounts b} -> {f : FrameBuffer c a ~ TFFrameBuffer b} -> b -> FrameBuffer c a
+testdata/scope01.reject.lc 2:17-2:46  FrameBuffer V2 V3
+testdata/scope01.reject.lc 2:29-2:46  Image 1 ('Color Float)
+testdata/scope01.reject.lc 2:30-2:41  {a:Nat} -> {b} -> {c} -> {d : Num b} -> {e : c ~ VecScalar a b} -> c -> Image 1 ('Color c)
+testdata/scope01.reject.lc 2:42-2:45  Float
+testdata/scope01.reject.lc 3:8-3:17  {a:Nat} -> {b : List ImageSemantics} -> FrameBuffer a b -> Output