G |- LAM. 2 ^ 1 <= (tm -> tm) -> tm      G |- tm-eq/i ^ (1 ^ (LAM. f ^ 1)) : PI tm-eq (M (LAM f ^ 1)) (M (LAM f ^ 1)). type >> type

---------------------------------------------------------------------------------------------------------------------------------------

(tm -> tm) -> tm |- (LAM. 2 ^ 1) 
                    tm-eq/i ^ (1 ^ (LAM. f ^ 1)) 
                 : PI (tm -> tm) -> tm. PI tm-eq (M (LAM f ^ 1)) (M (LAM f ^ 1)). type >> type

------------------------------------------------------------------------

(tm -> tm) -> tm |- test6 
                      (LAM. 2 ^ 1) 
                      tm-eq/i ^ (1 ^ (LAM. f ^ 1)) <= type

------------------------------------------------------------------------

PI (tm -> tm) -> tm. test6 
                      (LAM. 2 ^ 1) 
                      tm-eq/i ^ (1 ^ (LAM. f ^ 1)) <= type