Type Error (line 366)
In the context
a : Prop
b : [x:a1].Prop
a1 : (a1).(b).$ld:/l/and
not a function
(a1).(b).(a).$ld:/l/ande2