MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "InconsistentHypotheses.ma" ---
--- scope checking ---
--- type checking ---
type  f : .[i : Size] -> .[j < i] -> |i| < |j| -> Set
error during typechecking:
f
/// clause 1
/// adding size rel. v0 + 1 <= v1
/// cannot add hypothesis v0 + 1 <= v1 because it makes the set of hyptheses unsatisfiable