An exact proof term for the current goal is (PowerI EuclidPlane (affine_line_R2 a b c) (affine_line_R2_subset a b c)).