--- a/src/logic.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/logic.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -50,6 +50,19 @@
 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
 dont-orb {A} {B} (case1 a) ¬B = a
 
+open import Relation.Binary.PropositionalEquality
+
+¬i0≡i1 : ¬ ( i0 ≡ i1 )
+¬i0≡i1 ()
+
+¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 
+¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
+¬i0→i1 {i1} ne = refl
+
+¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
+¬i1→i0 {i0} ne = refl
+¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
+
 
 infixr  130 _∧_
 infixr  140 _∨_