Progress on [isconn_wedge_incl].
Added some lemmas on the interaction of ap with application and lambda.
Added a special nondependent case for transport_forall.
Added some lemmas.
Added lemmas.Merge branch 'master' of https://github.com/HoTT/HoTT
Completed crude proof of wedge-elim, modulo lemma on connectedness of point-inclusion.
Merge branch 'master' into connectedness
Changing names of Kristina's pull request
Merge pull request #107 from DanGrayson/master

fix a reference better
Merge pull request #108 from andrejbauer/master

Kristina's pull request with changed names
Connectedness: abstracted/reorganised some auxiliary lemmas.
Added lemmas that [projT1_path] preserves groupoid structure.
Somewhat improved proof of [isconn_wedge_incl].
Completed wedge-inclusion connectivity lemma; reorganised Connectedness slightly.
Moved [unit_name] and [concatR] out of Connectedness to better homes.
Merge branch 'master' into connectedness
Added tactic [equiv_via].
Minor documentaion/alignment updating.
Fixed issue with prev definition of [equiv_via].
Added [contr_arrow], [trunc_arrow].