implies to prop

cryspen · Feb 13, 2025 · 4017a79 · 4017a79
1 parent 71f256d
commit 4017a79
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst
@@ -1,3 +1,5 @@
 module Hax_lib.Prop
 
 type t_Prop = Type0
+
+unfold let implies (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs ()