(* senza questa change, universe inconsistency *)
change in ⊢ (? ? (λ_:%.?)) with (carr I);
exists [apply w1] exists [apply w] assumption;
(* senza questa change, universe inconsistency *)
change in ⊢ (? ? (λ_:%.?)) with (carr I);
exists [apply w1] exists [apply w] assumption;
[ assumption
| (* senza questa change, universe inconsistency *)
whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);
[ assumption
| (* senza questa change, universe inconsistency *)
whd; change in ⊢ (? ? (λ_:%.?)) with (carr I);