diff --git a/theories/encodings/encodable.v b/theories/encodings/encodable.v
index 142f944c7cac9ce903bac04dbb023b56fbf60bc6..bebe9fd32a1361cc324338b3cf11f77c675e3cb5 100644
--- a/theories/encodings/encodable.v
+++ b/theories/encodings/encodable.v
@@ -1,30 +1,7 @@
 From iris.heap_lang Require Import proofmode notation.
 
 Class Encodable A := encode : A -> val.
-Instance val_encodable : Encodable val := id.
-Instance int_encodable : Encodable Z := λ n, #n.
-Instance bool_encodable : Encodable bool := λ b, #b.
-Instance unit_encodable : Encodable unit := λ _, #().
-Instance loc_encodable : Encodable loc := λ l, #l.
-
 Class Decodable A := decode : val -> option A.
-Instance val_decodable : Decodable val := id $ Some.
-Instance int_decodable : Decodable Z :=
-  λ v, match v with
-       | LitV (LitInt z) => Some z
-       | _ => None
-       end.
-Instance bool_decodable : Decodable bool :=
-  λ v, match v with
-       | LitV (LitBool b) => Some b
-       | _ => None
-       end.
-Instance loc_decodable : Decodable loc :=
-  λ v, match v with
-       | LitV (LitLoc l) => Some l
-       | _ => None
-       end.
-
 Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
 {
   encdec : ∀ v, decode (encode v) = Some v;
@@ -33,26 +10,123 @@ Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
 
 Ltac solve_encdec := intros v; by unfold decode, encode.
 Ltac solve_decenc :=
-  intros v w H;
-  destruct v as [l | | | | ]; try by inversion H;
+  intros ?v ?w ?H;
+  destruct v as [?l | | | | ]; try by inversion H;
   destruct l; try by inversion H.
-
 Ltac solve_encdec_decenc :=
   split; [solve_encdec | solve_decenc].
 
+(* Instances *)
+Instance val_encodable : Encodable val := id.
+Instance val_decodable : Decodable val := id $ Some.
 Instance val_encdec : EncDec val.
 Proof.
   split.
   - intros v. unfold decode, encode. eauto.
   - intros v w H. by destruct v; inversion H.
 Qed.
+
+Instance int_encodable : Encodable Z := λ n, #n.
+Instance int_decodable : Decodable Z :=
+  λ v, match v with
+       | LitV (LitInt z) => Some z
+       | _ => None
+       end.
 Instance int_encdec : EncDec Z.
 Proof. solve_encdec_decenc. Qed.
+
+Instance bool_encodable : Encodable bool := λ b, #b.
+Instance bool_decodable : Decodable bool :=
+  λ v, match v with
+       | LitV (LitBool b) => Some b
+       | _ => None
+       end.
 Instance bool_encdec : EncDec bool.
 Proof. solve_encdec_decenc. Qed.
+
+Instance loc_encodable : Encodable loc := λ l, #l.
+Instance loc_decodable : Decodable loc :=
+  λ v, match v with
+       | LitV (LitLoc l) => Some l
+       | _ => None
+       end.
 Instance loc_encdec : EncDec loc.
 Proof. solve_encdec_decenc. Qed.
 
+Instance unit_encodable : Encodable unit := λ _, #().
+Instance unit_decodable : Decodable unit :=
+  λ v, match v with
+       | LitV (LitUnit) => Some ()
+       | _ => None
+       end.
+Instance unit_encdec : EncDec unit.
+Proof.
+  split.
+  - intros v. destruct v. by unfold decode, encode.
+  - solve_decenc.
+Qed.
+
+Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
+  λ p, (encode p.1, encode p.2)%V.
+Instance pair_decodable `{Decodable A, Decodable B} : Decodable (A * B) :=
+  λ v, match v with
+       | PairV v1 v2 => match decode v1, decode v2 with
+                        | Some v1, Some v2 => Some (v1, v2)
+                        | _, _ => None
+                        end
+       | _ => None
+       end.
+Instance pair_encdec `{EncDec A, EncDec B} : EncDec (A * B).
+Proof.
+  split.
+  - intros v. destruct v. unfold decode, encode. simpl.
+    rewrite encdec. rewrite encdec. reflexivity.
+  - intros v w Heq. destruct w.
+    unfold decode, encode in *.
+    unfold pair_encodable, pair_decodable in *. simpl.
+    destruct v; inversion Heq.
+    by f_equiv;
+    apply decenc;
+    destruct (decode v1); inversion Heq;
+    destruct (decode v2); inversion Heq.
+Qed.
+
+Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
+  match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
+Instance option_decodable `{Decodable A} : Decodable (option A) :=
+  λ v, match v with
+       | SOMEV v => match decode v with
+                    | Some v => Some (Some v)
+                    | None => None
+                    end
+       | NONEV => Some (None)
+       | _ => None
+       end.
+Instance option_encdec `{EncDec A} : EncDec (option A).
+Proof.
+  split.
+  - intros v. unfold decode, encode.
+    destruct v; simpl. rewrite encdec. eauto. eauto.
+  - intros v w Heq.
+    destruct w.
+    + unfold decode, encode in *.
+      unfold option_encodable, option_decodable in *.
+      destruct v; inversion Heq.
+      destruct v; inversion Heq.
+      destruct l; inversion Heq.
+      f_equiv.
+      apply decenc.
+        by destruct (decode v); inversion Heq.
+    + unfold decode, encode in *.
+      simpl.
+      unfold option_encodable, option_decodable in *.
+      destruct v; inversion Heq.
+      * destruct v; inversion Heq.
+        destruct l; inversion Heq.
+        eauto.
+      * destruct (decode v); inversion Heq.
+Qed.
+
 Lemma enc_dec {A : Type} `{ED : EncDec A}
       v (w : A) : encode w = v <-> decode v = Some w.
 Proof.
@@ -74,11 +148,4 @@ Proof.
   erewrite encdec in H=> //.
   erewrite encdec in H=> //.
   by inversion H.
-Qed.
-
-(* Common Functional structures *)
-Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
-  λ p, (encode p.1, encode p.2)%V.
-
-Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
-  match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
+Qed.
\ No newline at end of file