(* Advanced properties ******************************************************)
lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o).
(* Advanced properties ******************************************************)
lemma ffdeq_refl: ∀h,o. tri_reflexive … (ffdeq h o).