Prop:Type
by simp;by exact sorry

true:unit
trivial:star
is_true:is_unit

false:empty
is_false:is_empty

induction:rec
induction_on:rec_on

∨;⊎
or.elim:sum.rec_on
or.inl:sum.inl
or.inr:sum.inr
or.intro_left _;sum.inl
or.intro_right _;sum.inr
or_resolve_right:sum_resolve_right
or_resolve_left:sum_resolve_left
or.swap:sum.swap
or.rec_on:sum.rec_on
or_of_or_of_imp_of_imp:sum_of_sum_of_imp_of_imp
or_of_or_of_imp_left:sum_of_sum_of_imp_left
or_of_or_of_imp_right:sum_of_sum_of_imp_right

∧;×
and.intro:pair
and.left:
and.elim_left:prod.pr1
and.left:prod.pr1
and.elim_right:prod.pr2
and.right:prod.pr2

∀;Π

∃;Σ
exists.intro:sigma.mk
exists.elim:sigma.rec_on

eq.symm:inverse
congr_arg:ap