intro h1 h2
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
⊢ ↑f fst✝¹ = ↑f fst✝ → ↑f snd✝¹ = ↑f snd✝ → fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
case mk.mk.mk.mk
ι : Sort ?u.224451
𝕜 : Type ?u.224454
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : G →g G'
hinj : Injective ↑f
fst✝¹ snd✝¹ : V
h₁ : (fst✝¹, snd✝¹) ∈ edgeSet G
fst✝ snd✝ : V
h₂ : (fst✝, snd✝) ∈ edgeSet G
h1 : ↑f fst✝¹ = ↑f fst✝
h2 : ↑f snd✝¹ = ↑f snd✝
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝