Helper functions for constructing proof terms in the offset constraint procedure.
Returns a proof for true = true
Equations
Instances For
Assume pi₁
is { w := u, k := k₁, proof := p₁ }
and pi₂
is { w := w, k := k₂, proof := p₂ }
p₁
is the proof for edge u -(k₁) → w
and p₂
the proof for edge w -(k₂)-> v
.
Then, this function returns a proof for edge u -(k₁+k₂) -> v
.