From bf2876fde9b8fdd4aae286b4e077a47df45916f7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:33:48 +0100
Subject: Prove conversion subsumes reduction.

---
 src/Core/Reduction.idr | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src/Core')

diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 21e6ee5..54a4523 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -50,9 +50,26 @@ namespace Term
 -- Reduction Subsumed by Conversion --------------------------------------------
 
 termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a
+termStepImpliesTermConv (PiBeta wf wf1 wf2) = PiBeta wf wf1 wf2
+termStepImpliesTermConv (AppStep step wf) = AppConv (termStepImpliesTermConv step) (ReflTerm wf)
+termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTermConv step) conv
+
 typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
+typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step)
+
 typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
+typeRedImpliesTypeConv (Stay wf) = ReflType wf
+typeRedImpliesTypeConv (step :: steps) =
+  TransType
+    (typeStepImpliesTypeConv step)
+    (typeRedImpliesTypeConv steps)
+
 termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
+termRedImpliesTermConv (Stay wf) = ReflTerm wf
+termRedImpliesTermConv (step :: steps) =
+  TransTerm
+    (termStepImpliesTermConv step)
+    (termRedImpliesTermConv steps)
 
 -- Subject Typing --------------------------------------------------------------
 
-- 
cgit v1.2.3