rewrote one proof to use case_if tactic since I remembered it exists
changed ctx_hole type rule to concatenate environments instead of an arbitrary extends; finished proofs of basic source properties
updated t_context_typing