Судебное равенство

TL; DR: в Agda, учитывая a : A и proof : A == B, могу ли я получить элемент a : B?

В моей постоянной попытке изучить Agda я создал следующий тип данных Prime : nat -> Set, который свидетельствует о примитивности естественного.

Prime zero = False
Prime (succ zero) = False
Prime (succ (succ n)) = forall {i : nat} -> divides i p -> i <N p -> zero <N i -> i == (succ zero)
  where
    p = succ (succ n)

Здесь:

• False - это тип данных без конструкторов;
• divides a b - это тип данных, который содержит свидетельство k о том, что a * k = b;
• a <N b - это тип данных, который содержит свидетельство k о том, что a + k = b;
• == - это тип равенства, только с одним конструктором refl;
• натуральные числа определяются очевидным образом с помощью zero : nat и succ : nat -> nat.

Я успешно выставил член Prime (succ (succ zero)) и доказал, что утверждение Prime (succ (succ (succ (succ zero))))) подразумевает False.

Теперь я пытаюсь доказать, что простые числа больше единицы:

primesAreGreaterThanOne : (p : Sg nat Prime) -> (succ zero <N value p)

где

• Sg A pred представляет собой зависимую пару (p, pred(p)), где p : A;
• value : Sg A pred -> A извлекает значение и отбрасывает доказательство.

Я уже доказал трихотомию порядка: для всех a, b верно либо то, что a <N b, либо a == b, либо b <N a. (Надеюсь, эта лемма поможет нам избежать проблем с исключенным средним). Итак, работая над отношением упорядочения между succ zero и value p, я свелся к случаю, когда у меня есть доказательство p == zero и доказательство Prime p. и утверждение, что Prime zero определено как ложное.

Конечно, эти утверждения противоречивы: поскольку у меня есть доказательство того, что p == zero, я могу выставлять обитателя типа Prime p == Prime zero, а значит, у меня есть обитатель Prime p == False.

Но как я могу взять свой элемент proof : Prime p (доказательство, которое является вторым компонентом p : Sg nat Prime) и «привязать» его к элементу False? Типы теоретически равны, но не равны с точки зрения суждений.