fact: Definition RU2SemiU : term * term * term -> Prop := fun '(s0, s1, t) => exists (φ ψ0 ψ1: valuation), substitute ψ0 (substitute φ s0) = substitute φ t /\ substitute ψ1 (substitute φ s1) = substitute φ t.
imports: List