proposition: Lemma proj_uniqueness : forall A B T P P', proj T A B P -> proj T A B P' -> P = P'.
proof: Proof. intros. unfold proj in *. spliter. induction H1; induction H2; spliter; assert(Col A P P'). ColR. eapply (l8_18_uniqueness A B T P P'); auto. subst T. contradiction. contradiction. subst P'. ColR. subst P'. contradiction. subst T. subst P'. Col. subst T. subst P'. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec