proposition: Lemma multistep_Pair {Γ τ1 τ2} {e1 e1' : Γ ⊢ τ1} {e2 e2' : Γ ⊢ τ2} : ValueP e1' → (e1 --->* e1') → (e2 --->* e2') → Pair e1 e2 --->* Pair e1' e2'.
proof: Proof. intros. erewrite multistep_Pair1; eauto. erewrite multistep_Pair2; eauto. now apply multi_refl. Qed.
imports: Category.Lib Category.Instance.Lambda.Ltac Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Category.Instance.Lambda.Sem Category.Instance.Lambda.Step Equations(Equations)