Theorem: HTPI.seq_cons_def (HTPILib/Chap8Part2.lean)

State before:
U : Type
x : U
l : List U
⊢ seq_cons U (x, l) = x :: l
Tactic:
rfl
State after:
no goals