fsdoc: no-summary-found
fsdoc: no-comment-found
val closure_step:Unidentified product: [#a:Type0] Unidentified product: [r:relation a] Unidentified product: [x:a] Unidentified product: [y:a] (Lemma ((requires r x y)) ((ensures closure r x y)) (Prims.Cons (SMTPat (closure r x y)) (Prims.Nil )))closure r includes r
val closure_inversion:Unidentified product: [#a:Type0] Unidentified product: [r:relation a] Unidentified product: [x:a] Unidentified product: [y:a] (Lemma ((requires closure r x y)) ((ensures \/(==(x, y), (exists z.{:pattern } /\(r x z, closure r z y))))) (Prims.Cons (SMTPat (closure r x y)) (Prims.Nil )))closure r is the smallest preorder that includes r
val stable_on_closure:Unidentified product: [#a:Type0] Unidentified product: [r:relation a] Unidentified product: [p:(Unidentified product: [a] Type0)] Unidentified product: [p_stable_on_r:(squash (forall x y.{:pattern (p y); (r x y)} ==>(/\(p x, r x y), p y)))] (Lemma (forall x y.{:pattern (closure r x y)} ==>(/\(p x, closure r x y), p y)))r is stable on closure r