Theorem silly1 : forall (n m o p : nat),
  n = m  ->
  [n;o] = [n;p] ->
  [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.
  apply eq2.  Qed.

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
  reflexivity.  Qed.

Theorem silly3' : forall (n : nat),
  (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
  true = beq_nat n 5  ->
  true = beq_nat (S (S n)) 7.
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H.  Qed.

Theorem example_1 : forall A B, (A -> B) -> A -> B.
Proof. intros ? ? H1. apply H1. Qed.

Theorem example_2 : forall A B, (A -> B) -> A -> B.
Proof. intros ? ? H1 H2. apply H1. apply H2. Qed.

Print example_1.
Print example_2.

Fixpoint reverse_helper {A : Type} (l1 l2 : list A) : list A :=
  match l1 with
  | nil => l2
  | cons x l1 => reverse_helper l1 (cons x l2)
  end.

Theorem example_3 : forall A (l1 l2 : list A), reverse_helper l1 l2 = app (reverse_helper l1 nil) l2.
Proof. intros. induction l1. simpl. reflexivity. simpl. try rewrite IHl1. Abort.

Theorem example_4 : forall A (l1 l2 : list A), reverse_helper l1 l2 = app (reverse_helper l1 nil) l2.
Proof. induction l1. intros. simpl. reflexivity. intros. simpl. rewrite (IHl1 (cons a l2)). rewrite (IHl1 (cons a nil)). Admitted.

H1 : A1
...
Hn : An
___
B

H1: A1, ..., Hn: An ⊢ B.