Experiment with SProp to make gmap operations compute nicely

Currently both Pmap and gmap are sigma types of the form {x:T | Is_true (wf x : bool)}. If they were instead written {x:T | sis_true (wf x : bool) : SProp} (using sis_true (b:bool) : SProp := if b then sUnit else sEmpty), then the well-formedness proof would be in SProp. This gives not just proof irrelevance but definitional proof irrelevance, which I think means proofs will compute away properly when reducing gmap operations in Coq.