proposition: Lemma pjf_1 : forall (i : nat) Hi Hi', partition_join_fun i Hi [=] P i Hi'.
proof: Proof. intros; unfold partition_join_fun in |- *. elim le_lt_dec; intro; simpl in |- *. apply prf1; auto. exfalso; apply Nat.le_ngt with i n; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)