antonatoss: not really a proof term 2.1
antonidesam: using tactic mode in 1.2 (half points?)
arininurrohmah: 2.1 same as antonatoss, but just uses assume
basaraa: something about choice? i don't really know about choice though
ceuppensqnc: using tactic mode in 1.2
khanna: 2.1 is technically tactical, 2.2 is nonsense, 1.2 is.. uhh.. idk, 1.1 is backward

garifollinad, knyajevd, mullaim: all have the same answer for weak_peirce2?
                                 with the same 'typo'?
                                 and same answer for exists_and_commute

nadifa also has veerry similar answer for exists_and_commute (especially the
have qp: _ and show _, from ... are strangely similar) but is not exact



kreuzensec: kind of just doesn't seem to get it

sklavosa: uses `by cc` in 1.2, but it is a tiny bit of the proof (-1p)

-- general:
Using fix in 2.1?
I think people got confused by `namespace backward_proofs` for 1.1
