From adad5280af0d81a2f171df619e9c7169dcb43a02 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 27 Mar 2021 20:32:03 +0000
Subject: Introduce non-terminating proof of derivation existence.

---
 src/Cfe/Language/Indexed/Construct/Iterate.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Cfe/Language/Indexed')

diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 1a37326..0ae9100 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -73,6 +73,9 @@ module _
     where
     module Iter = IndexedLanguage (Iterate f)
 
+  fⁿ≤⋃f : ∀ f n → (f ^ n) (Lift a ∅) ≤ ⋃ f
+  fⁿ≤⋃f f n = record { f = n ,_ }
+
   ⋃-cong : ∀ {f g} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g
   ⋃-cong f≈g = record
     { f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈fn}
-- 
cgit v1.2.3