Started working on "judged expressions".

Here is the idea, partially implemented, as explained at the bottom of the file README:

    Context:

	 beta_reduction' : (T:a_type) ⟶ (o1:obj_of_type T) ⟶ (U:obj_of_type T ⟶ a_type) ⟶ (o2:(t:obj_of_type T) ⟶ obj_of_type (U t)) ⟶ judged_obj_equal (U o1) (ev_hastype' T U (lambda_hastype' T U o2) o1) (o2 o1)
	 ev_hastype' : (T:a_type) ⟶ (U:obj_of_type T ⟶ a_type) ⟶ obj_of_type (Pi_istype' T U) ⟶ (o:obj_of_type T) ⟶ obj_of_type (U o)
	 lambda_hastype' : (T:a_type) ⟶ (U:obj_of_type T ⟶ a_type) ⟶ ((t:obj_of_type T) ⟶ obj_of_type (U t)) ⟶ obj_of_type (Pi_istype' T U)
	 El_u_reduction' : (M:uexp) ⟶ judged_type_equal (El_istype' M (u_hastype' M)) (U_istype' M)
	 El_istype' : (M:uexp) ⟶ obj_of_type (U_istype' M) ⟶ a_type
	 u_hastype' : (M:uexp) ⟶ obj_of_type (U_istype' ([next] M))
	 U_istype' : uexp ⟶ a_type
	 Pi_istype' : (T:a_type) ⟶ (obj_of_type T ⟶ a_type) ⟶ a_type

    Signature:

      Kind constants:
	 expression : kind
	 judgment : kind
	 judged_expression : kind
	 judged_expression_judgment : kind

      Type family constants:
	 uexp : expression
	 texp : expression
	 oexp : expression
	 istype : texp ⟶ judgment
	 hastype : oexp ⟶ texp ⟶ judgment
	 uequal : uexp ⟶ uexp ⟶ judgment
	 tequal : texp ⟶ texp ⟶ judgment
	 oequal : oexp ⟶ oexp ⟶ texp ⟶ judgment
	 tuequal : texp ⟶ texp ⟶ judgment
	 ouequal : oexp ⟶ oexp ⟶ texp ⟶ judgment
	 a_type : judged_expression
	 obj_of_type : a_type ⟶ judged_expression
	 judged_type_equal : a_type ⟶ a_type ⟶ judged_expression_judgment
	 judged_obj_equal : (T:a_type) ⟶ obj_of_type T ⟶ obj_of_type T ⟶ judged_expression_judgment

      Object constants:
	 [∏] : texp ⟶ (oexp ⟶ texp) ⟶ texp
	 [Σ] : texp ⟶ (oexp ⟶ texp) ⟶ texp
	 [∐] : texp ⟶ texp ⟶ texp
	 [λ] : texp ⟶ (oexp ⟶ oexp) ⟶ oexp
	 [∀] : uexp ⟶ uexp ⟶ oexp ⟶ (oexp ⟶ oexp) ⟶ oexp
	 [next] : uexp ⟶ uexp
	 [max] : uexp ⟶ uexp ⟶ uexp
	 [El] : oexp ⟶ texp
	 [U] : uexp ⟶ texp
	 [∏] : texp ⟶ (oexp ⟶ texp) ⟶ texp
	 [Σ] : texp ⟶ (oexp ⟶ texp) ⟶ texp
	 [Pt] : texp
	 [∐] : texp ⟶ texp ⟶ texp
	 [Coprod2] : texp ⟶ texp ⟶ (oexp ⟶ texp) ⟶ (oexp ⟶ texp) ⟶ texp
	 [Empty] : texp
	 [IP] : texp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ oexp ⟶ oexp) ⟶ texp
	 [Id] : texp ⟶ oexp ⟶ oexp ⟶ texp
	 [u] : uexp ⟶ oexp
	 [j] : uexp ⟶ uexp ⟶ oexp
	 [ev] : oexp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ oexp
	 [λ] : texp ⟶ (oexp ⟶ oexp) ⟶ oexp
	 [∀] : uexp ⟶ uexp ⟶ oexp ⟶ (oexp ⟶ oexp) ⟶ oexp
	 [pair] : oexp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ oexp
	 [pr1] : texp ⟶ (oexp ⟶ texp) ⟶ oexp ⟶ oexp
	 [pr2] : texp ⟶ (oexp ⟶ texp) ⟶ oexp ⟶ oexp
	 [total] : uexp ⟶ uexp ⟶ oexp ⟶ (oexp ⟶ oexp) ⟶ oexp
	 [pt] : oexp
	 [pt_r] : oexp ⟶ (oexp ⟶ texp) ⟶ oexp
	 [tt] : oexp
	 [coprod] : uexp ⟶ uexp ⟶ oexp ⟶ oexp ⟶ oexp
	 [ii1] : texp ⟶ texp ⟶ oexp ⟶ oexp
	 [ii2] : texp ⟶ texp ⟶ oexp ⟶ oexp
	 [sum] : texp ⟶ texp ⟶ oexp ⟶ oexp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ oexp
	 [empty] : oexp
	 [empty_r] : texp ⟶ oexp ⟶ oexp
	 [c] : texp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ oexp ⟶ oexp) ⟶ oexp ⟶ oexp ⟶ oexp
	 [ip_r] : texp ⟶ oexp ⟶ (oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ texp) ⟶ (oexp ⟶ oexp ⟶ oexp ⟶ oexp) ⟶ oexp ⟶ (oexp ⟶ oexp ⟶ texp) ⟶ oexp ⟶ oexp
	 [ip] : oexp ⟶ oexp ⟶ (oexp ⟶ oexp) ⟶ (oexp ⟶ oexp ⟶ oexp) ⟶ (oexp ⟶ oexp ⟶ oexp ⟶ oexp) ⟶ oexp
	 [paths] : texp ⟶ oexp ⟶ oexp ⟶ oexp
	 [refl] : texp ⟶ oexp ⟶ oexp
	 [J] : texp ⟶ oexp ⟶ oexp ⟶ oexp ⟶ oexp ⟶ (oexp ⟶ oexp ⟶ texp) ⟶ oexp
	 [rr0] : uexp ⟶ uexp ⟶ oexp ⟶ oexp ⟶ oexp ⟶ oexp
	 [rr1] : uexp ⟶ oexp ⟶ oexp ⟶ oexp