Fix errors

theories/Core/Completeness/ContextCases.v

@@ -22,12 +22,10 @@ Proof with intuition.
   destruct_conjs.
   handle_per_ctx_env_irrel.
   eexists.
-  econstructor; eauto with typeclass_instances.
+  per_ctx_env_econstructor; eauto.
   - instantiate (1 := fun p p' (equiv_p_p' : env_relΓ p p') m m' =>
-                        forall i a a' R,
-                          {{ ⟦ A ⟧ p ↘ a }} ->
-                          {{ ⟦ A' ⟧ p' ↘ a' }} ->
-                          per_univ_elem i R a a' ->
+                        forall i R,
+                          rel_typ i A p A' p' R ->
                           R m m').
     intros.
     (on_all_hyp: destruct_rel_by_assumption env_relΓ).
@@ -37,6 +35,8 @@ Proof with intuition.
     destruct_conjs.
     econstructor; eauto.
     apply -> per_univ_elem_morphism_iff; eauto.
-    split; intros; handle_per_univ_elem_irrel...
+    split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
+    eapply H12.
+    econstructor...
   - apply Equivalence_Reflexive.
 Qed.

theories/Core/Completeness/FunctionCases.v

@@ -18,22 +18,22 @@ Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
         rel_exp B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (per_univ i)) ->
     (* We use this equality to make unification on `out_rel` works *)
     (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
-                 forall b b' R',
-                   {{ ⟦ B ⟧ o ↦ c ↘ b }} ->
-                   {{ ⟦ B' ⟧ o' ↦ c' ↘ b' }} ->
-                   per_univ_elem i R' b b' -> R' m m') ->
+                 forall R',
+                   rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R' ->
+                   R' m m') ->
     (forall c c' (equiv_c_c' : R c c'), rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (out_rel c c' equiv_c_c')).
 Proof with intuition.
   pose proof (@relation_equivalence_pointwise domain).
   pose proof (@relation_equivalence_pointwise env).
   intros.
   subst.
   (on_all_hyp: destruct_rel_by_assumption R).
-  destruct_by_head rel_exp.
   econstructor; mauto.
   destruct_by_head per_univ.
   apply -> per_univ_elem_morphism_iff; eauto.
-  split; intros; handle_per_univ_elem_irrel...
+  split; intros; destruct_by_head rel_typ; handle_per_univ_elem_irrel...
+  eapply H5.
+  econstructor...
 Qed.
 
 Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
@@ -153,6 +153,7 @@ Proof with intuition.
     extract_output_info_with p c p' c' env_relΓA.
     econstructor; only 1-2: repeat econstructor; eauto.
     intros.
+    destruct_by_head rel_typ.
     handle_per_univ_elem_irrel...
 Qed.
 
@@ -189,8 +190,9 @@ Proof with intuition.
       apply Equivalence_Reflexive.
   - intros ? **.
     extract_output_info_with o c o' c' env_relΔA.
-    econstructor; only 1-2: repeat econstructor; simpl; mauto.
+    econstructor; only 1-2: repeat econstructor; mauto.
     intros.
+    destruct_by_head rel_typ.
     handle_per_univ_elem_irrel...
 Qed.
 

theories/Core/Completeness/SubstitutionCases.v

@@ -57,8 +57,7 @@ Proof with intuition.
   pose (env_relΔA0 := env_relΔA).
   handle_per_ctx_env_irrel.
   eexists_rel_subst.
-  match_by_head (per_ctx_env env_relΔA)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+  match_by_head (per_ctx_env env_relΔA) invert_per_ctx_env.
   destruct_conjs.
   handle_per_ctx_env_irrel.
   intros.
@@ -134,8 +133,7 @@ Proof with intuition.
   pose (env_relΓ''A0 := env_relΓ''A).
   handle_per_ctx_env_irrel.
   eexists_rel_subst.
-  match_by_head (per_ctx_env env_relΓ''A)
-    ltac:(fun H => eapply per_ctx_env_cons_clear_inversion in H; [| eassumption]).
+  match_by_head (per_ctx_env env_relΓ''A) invert_per_ctx_env.
   destruct_conjs.
   handle_per_ctx_env_irrel.
   intros.