Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
- (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *)
- apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto.
+ (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
+ apply nd_rule; apply (org_fc _ _ (RVoid _ _ )). auto.
(* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
(* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto.
- (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *)
+ (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ].
eapply nd_comp; [ apply nd_llecnac | idtac ].
(* nd_cancell becomes RVar;;RuCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
(* nd_cancell becomes RVar;;RuCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ].
auto.
(* nd_cancelr becomes RVar;;RuCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
auto.
(* nd_cancelr becomes RVar;;RuCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ].
auto.
(* nd_llecnac becomes RVar;;RCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
auto.
(* nd_llecnac becomes RVar;;RCanL *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ].
auto.
(* nd_rlecnac becomes RVar;;RCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
auto.
(* nd_rlecnac becomes RVar;;RCanR *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ].
auto.
(* nd_assoc becomes RVar;;RAssoc *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
auto.
(* nd_assoc becomes RVar;;RAssoc *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
auto.
(* nd_cossa becomes RVar;;RCossa *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
auto.
(* nd_cossa becomes RVar;;RCossa *)
eapply nd_comp;
[ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
| PCF_RLam Σ tx te => let case_RLam := tt in _
| PCF_RApp Σ tx te p => let case_RApp := tt in _
| PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
| PCF_RLam Σ tx te => let case_RLam := tt in _
| PCF_RApp Σ tx te p => let case_RApp := tt in _
| PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
- | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _
- | PCF_REmptyGroup => let case_REmptyGroup := tt in _
+ | PCF_RJoin b c d e => let case_RJoin := tt in _
+ | PCF_RVoid => let case_RVoid := tt in _
(*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
(*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
end); simpl in *.
(*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
(*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
end); simpl in *.