proposition: Lemma E2_ind s t ρ1 ρ2 p : (forall P Q, E s ρ1 P -> E t ρ2 Q -> (forall P', step P P' -> p P' Q) -> (forall Q', step Q Q' -> p P Q') -> p P Q) -> forall P Q, E s ρ1 P -> E t ρ2 Q -> p P Q.
proof: Proof. intros H P Q. induction 1 in Q |- *. induction 1. eapply H; eauto using R. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms