proposition: Lemma fun_seq_minus_helper A (R S T: relation A) (FUN: functional R): R ⨾ (S \ T) ≡ (R ⨾ S) \ (R ⨾ T).
proof: Proof. red; unfold minus_rel, seq, inclusion, transp, eqv_rel in *; splits; ins; desf; firstorder. intro; desf. assert (z=z0); try by subst. eapply FUN; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets