From 03747b58614b91257ea766517303a5834fd07497 Mon Sep 17 00:00:00 2001
From: hondet <hondet@nancy.private.lsv.fr>
Date: Sun, 11 Oct 2020 12:23:29 +0200
Subject: [PATCH] Reduction rule in star, variable

---
 encodings/bool_plus.lp | 3 +--
 encodings/cert_star.lp | 4 +++-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/encodings/bool_plus.lp b/encodings/bool_plus.lp
index cf1b187..7aac76c 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 1ceddc8..a89c98b 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
 
-- 
GitLab