abstract out some idioms for dealing with decidable types#1956

Alizter merged 2 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom

Alizter:ps/rr/abstract_out_some_idioms_for_dealing_with_decidable_typesAlizter/HoTT:ps/rr/abstract_out_some_idioms_for_dealing_with_decidable_typesCopy head branch name to clipboard