An exact proof term for the current goal is (PowerI (setprod R R) (affine_line_R2 a b c) (affine_line_R2_subset_R2 a b c)).