cert star, reduced dependencies

encodings/bool_plus.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.prenex
+require open personoj.encodings.bool_hol
+
+// It may be generalisable to dependent propositions
+theorem and_intro:
+  Prf
+  (∀ {bool} (λa,
+   ∀ {bool} (λb,
+   a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b))))))
+proof
+  assume A B h0 h1 f
+  refine f h0 h1
+qed
+
+theorem and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a
+proof
+  assume a b h
+qed

encodings/cert_star.lp

@@ -33,10 +33,10 @@ set infix left 2 "~" ≔ compatible
 definition comp_refl t ≔ eqv_refl (pull t)
 
 protected symbol same' {t: Set} (u: Set) (_: El t): El u
+rule same' $t $t $m ↪ $m
 definition same {t: Set} (u: Set) (_: Prf (equivalent t u)) (m: El t)
          ≔ same' u m
 
-rule same' $t $t $m ↪ $m
 
 definition cast {fr_t: Set} (to_t: Set) (comp: Prf (fr_t ~ to_t))
                 (m: El fr_t)

encodings/prenex.lp

@@ -6,7 +6,6 @@
 /// For more informations on the encoding of prenex polymorphism, see
 /// https://arxiv.org/abs/1807.01873 and theory U
 require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
 
 // Quantification for objects of type ‘Kind’
 set declared "ϕ"