diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index cf1b1875fe4d97e5226f3a9b477e1b75053c6782..7aac76c27bad58d04ee09e3aa7790cbe540a6747 100644
--- a/encodings/bool_plus.lp
+++ b/encodings/bool_plus.lp
@@ -15,5 +15,4 @@ qed
 
 theorem and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a
 proof
-  assume a b h
-qed
+admit
diff --git a/encodings/cert_star.lp b/encodings/cert_star.lp
index 1ceddc8442c03ceadd1095c85278af604e8b093f..a89c98b147ddb90af961b358250ddc79c8c55d93 100644
--- a/encodings/cert_star.lp
+++ b/encodings/cert_star.lp
@@ -18,11 +18,13 @@ symbol fst {t: Set} (_: El t): El (pull t)
 symbol pair' (t: Set) (_: El (pull t)): El t
 definition pair t m (_: Prf (tcc t m)) ≔ pair' t m
 
+rule fst (pair' _ $m) ↪ $m
+
 rule tcc (psub {$t} $a) $x
    ↪ (tcc $t $x) ∧ (λy: Prf (tcc $t $x), $a (pair $t $x y))
 
 rule pull bool ↪ bool
-rule tcc bool $x ↪ true
+rule tcc bool _ ↪ true
 rule fst {bool} $x ↪ $x
 rule pair' bool $x _ ↪ $x