fact: Definition LU2SemiU : term * term * term -> Prop := fun '(s, t0, t1) => exists (φ ψ0 ψ1: valuation), substitute ψ0 (substitute φ s) = substitute φ t0 /\ substitute ψ1 (substitute φ s) = substitute φ t1.
imports: List