да это я вслух радуюсь своим маленьким находкам :)

последнее "истинно" относилось к тому, что когда стрелки A → ⊥ нет, то получаем множество таким стрелок не населено, и выражение сводится к ⊥ → (A → B). Это множество населено, т.к. есть стрелки из ⊥ во что угодно из рассуждений о A = ⊥. Тут забавно также, что доказывается существование стрелки из любого типа в любой другой. А маленькая находка в том, как правила импликации тоже выходят сами собой (из абсурда следует что угодно).