style

encodings/pvs_cert_minus.lp

@@ -4,7 +4,7 @@ require open personoj.encodings.lhol
 set declared "Σ"
 constant symbol Σ (T : Set): (η T → Set) → Set
 constant symbol pair {T: Set} {U: η T → Set} (M: η T) (_: η (U M))
-: η (Σ T U)
+              : η (Σ T U)
 
 symbol fst {T: Set} {U: η T → Set}: η (Σ T U) → η T
 rule fst (pair $M _) ↪ $M