val elim_calc_chain (#a: _) (rs: list (relation a)) (#x #y: a) (pf: calc_chain rs x y)
    : Lemma (ensures (calc_chain_related rs x y))
let rec elim_calc_chain #a (rs:list (relation a)) (#x #y:a) (pf:calc_chain rs x y)
  : Lemma (ensures (calc_chain_related rs x y))
  = let steps = [delta_only [`%calc_chain_related]; iota; zeta] in
    let t = norm steps (calc_chain_related rs x y) in
    norm_spec steps (calc_chain_related rs x y);
    match pf with
    | CalcRefl -> ()
    | CalcStep tl pf _ -> elim_calc_chain tl pf
val elim_calc_chain (#a: _) (rs: list (relation a)) (#x #y: a) (pf: calc_chain rs x y)
    : Lemma (ensures (calc_chain_related rs x y))
let rec elim_calc_chain #a (rs: list (relation a)) (#x: a) (#y: a) (pf: calc_chain rs x y)
    : Lemma (ensures (calc_chain_related rs x y)) =
let steps = [delta_only [`%calc_chain_related]; iota; zeta] in
let t = norm steps (calc_chain_related rs x y) in
norm_spec steps (calc_chain_related rs x y);
match pf with
| CalcRefl -> ()
| CalcStep tl pf _ -> elim_calc_chain tl pf
FStar.Calc.fst.checked
prims.fst.checked FStar.Squash.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
FStar.Calc.fst
Prims.list FStar.Preorder.relation FStar.Calc.calc_chain Prims.squash FStar.Calc.elim_calc_chain Prims.unit FStar.Pervasives.norm_spec FStar.Calc.calc_chain_related FStar.Pervasives.norm FStar.Pervasives.norm_step Prims.Cons FStar.Pervasives.delta_only Prims.string Prims.Nil FStar.Pervasives.iota FStar.Pervasives.zeta Prims.l_True FStar.Pervasives.pattern
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.

   Authors: Guido Martinez, Aseem Rastogi, Nikhil Swamy
*)

module FStar.Calc

open FStar.Squash
open FStar.Preorder

noeq
type calc_chain #a : list (relation a) -> a -> a -> Type =
  | CalcRefl : #x:a -> calc_chain [] x x
  | CalcStep :
    rs:(list (relation a)) -> #p:(relation a) ->
    #x:a -> #y:a -> #z:a -> calc_chain rs x y -> squash (p y z) -> calc_chain (p::rs) x z

let rec elim_calc_chain #a (rs:list (relation a)) (#x #y:a) (pf:calc_chain rs x y)
val elim_calc_chain (#a: _) (rs: list (relation a)) (#x #y: a) (pf: calc_chain rs x y)
    : Lemma (ensures (calc_chain_related rs x y))
rs: Prims.list (FStar.Preorder.relation a) -> pf: FStar.Calc.calc_chain rs x y
  -> FStar.Pervasives.Lemma (ensures FStar.Calc.calc_chain_related rs x y)