proposition: Lemma sep__sep_fun_i_wd : forall i j : nat, i = j -> forall (Hi : i <= n) (Hj : j <= n), sep__sep_fun_i i Hi[=]sep__sep_fun_i j Hj.
proof: Proof. do 3 intro. rewrite <- H. intros. unfold sep__sep_fun_i in |- *. elim (sep__sep_aux_lemma i); intros; simpl in |- *. apply bin_op_wd_unfolded; [ apply prf1; auto | algebra ]. apply prf1; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions