fiveIsFive : 5 = 5fiveIsFive = Refl twoPlusTwo : 2 + 2 = 4twoPlusTwo = Refl -- twoPlusTwoBad : 2 + 2 = 5-- twoPlusTwoBad = Refl disjoint : (n : Nat) -> Z = S n -> Voiddisjoint n prf = replace {p = disjointTy} prf ()  where    disjointTy : Nat -> Type    disjointTy Z = ()    disjointTy (S k) = Void plusReduces : (n:Nat) -> plus Z n = nplusReduces n = Refl plusReducesR : (n:Nat) -> plus n Z = nplusReducesR n = Refl plusReducesZ : (n:Nat) -> n = plus n ZplusReducesZ Z = ReflplusReducesZ (S k) = cong S (plusReducesZ k) plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)plusReducesS Z m = ReflplusReducesS (S k) m = cong S (plusReducesS k m)