Implement checking for sigmas

[jonsterling]

• Type formation
• Introduction: Pair
• Elimination: Spread
• Also, Spread needs a first parameter which is the motive. So the elimination rule needs to look like this:

     Γ !-[Σ;E] p : Σ[x:A]B             
     Γ, x : Σ[x:A]B !-[Σ;E] C : U
     Γ, u:A, v:[u/x]B !-[Σ;E] M : [<u,v>/x]C
-----------------------------------------------------
     Γ !-[Σ;E] spread([x]C; [u,v]M; p) : [p/x]C

Therefore, we have in the syntax:

Spread :: (B.Scope () Tm a) -> (B.Scope Bool Tm a) -> Tm a -> Tm a