- (* nd_comp becomes pl_subst (aka nd_cut) *)
- eapply nd_comp.
- apply (nd_llecnac ;; nd_prod IHX1 IHX2).
- clear IHX1 IHX2 X1 X2.
- apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
-
- (* nd_cancell becomes RVar;;RuCanL *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_cancelr becomes RVar;;RuCanR *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_llecnac becomes RVar;;RCanL *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_rlecnac becomes RVar;;RCanR *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_assoc becomes RVar;;RAssoc *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_cossa becomes RVar;;RCossa *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- destruct r as [r rp].
- rename h into h'.
- rename c into c'.
- rename r into r'.
-
- refine (match rp as R in @Rule_PCF _ _ _ H C _
- return
- ND (OrgR Γ Δ) []
- [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
- (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
- with
- | PCF_RArrange h c r q => let case_RURule := tt in _
- | PCF_RLit lit => let case_RLit := tt in _
- | PCF_RNote Σ τ n => let case_RNote := tt in _
- | PCF_RVar σ => let case_RVar := 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_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 *.
- clear rp h' c' r'.
-
- rewrite (unlev_lemma h (ec::nil)).
- rewrite (unlev_lemma c (ec::nil)).
- destruct case_RURule.
- refine (match q as Q in Arrange H C
- return
- H=(h @@@ (ec :: nil)) ->
- C=(c @@@ (ec :: nil)) ->
- ND (OrgR Γ Δ) []
- [sequent
- [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
- [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
- with
- | RLeft a b c r => let case_RLeft := tt in _
- | RRight a b c r => let case_RRight := tt in _
- | RCanL b => let case_RCanL := tt in _
- | RCanR b => let case_RCanR := tt in _
- | RuCanL b => let case_RuCanL := tt in _
- | RuCanR b => let case_RuCanR := tt in _
- | RAssoc b c d => let case_RAssoc := tt in _
- | RCossa b c d => let case_RCossa := tt in _
- | RExch b c => let case_RExch := tt in _
- | RWeak b => let case_RWeak := tt in _
- | RCont b => let case_RCont := tt in _
- | RComp a b c f g => let case_RComp := tt in _
- end (refl_equal _) (refl_equal _));
- intros; simpl in *;
- subst;
- try rewrite <- unlev_lemma in *.
-
- destruct case_RCanL.
- apply magic.
- apply ga_uncancell.
-
- destruct case_RCanR.
- apply magic.
- apply ga_uncancelr.